Index: kernel/arch/amd64/src/amd64.c
===================================================================
--- kernel/arch/amd64/src/amd64.c	(revision 7e752b2a0d66c871748e5fa9e8bbe3a27c70a202)
+++ kernel/arch/amd64/src/amd64.c	(revision 0bff73aed85c65c908499a83db3b7a8e89c7b3fc)
@@ -256,5 +256,5 @@
  * we need not to go to CPL0 to read it.
  */
-unative_t sys_tls_set(unative_t addr)
+sysarg_t sys_tls_set(sysarg_t addr)
 {
 	THREAD->arch.tls = addr;
Index: kernel/arch/amd64/src/debugger.c
===================================================================
--- kernel/arch/amd64/src/debugger.c	(revision 7e752b2a0d66c871748e5fa9e8bbe3a27c70a202)
+++ kernel/arch/amd64/src/debugger.c	(revision 0bff73aed85c65c908499a83db3b7a8e89c7b3fc)
@@ -125,5 +125,5 @@
 	
 	/* Disable breakpoint in DR7 */
-	unative_t dr7 = read_dr7();
+	sysarg_t dr7 = read_dr7();
 	dr7 &= ~(0x02U << (curidx * 2));
 	
@@ -152,15 +152,15 @@
 		if (!(flags & BKPOINT_INSTR)) {
 #ifdef __32_BITS__
-			dr7 |= ((unative_t) 0x03U) << (18 + 4 * curidx);
+			dr7 |= ((sysarg_t) 0x03U) << (18 + 4 * curidx);
 #endif
 			
 #ifdef __64_BITS__
-			dr7 |= ((unative_t) 0x02U) << (18 + 4 * curidx);
+			dr7 |= ((sysarg_t) 0x02U) << (18 + 4 * curidx);
 #endif
 			
 			if ((flags & BKPOINT_WRITE))
-				dr7 |= ((unative_t) 0x01U) << (16 + 4 * curidx);
+				dr7 |= ((sysarg_t) 0x01U) << (16 + 4 * curidx);
 			else if ((flags & BKPOINT_READ_WRITE))
-				dr7 |= ((unative_t) 0x03U) << (16 + 4 * curidx);
+				dr7 |= ((sysarg_t) 0x03U) << (16 + 4 * curidx);
 		}
 		
@@ -227,5 +227,5 @@
 	if (!(breakpoints[slot].flags & BKPOINT_INSTR)) {
 		if ((breakpoints[slot].flags & BKPOINT_CHECK_ZERO)) {
-			if (*((unative_t *) breakpoints[slot].address) != 0)
+			if (*((sysarg_t *) breakpoints[slot].address) != 0)
 				return;
 			
@@ -234,5 +234,5 @@
 		} else {
 			printf("Data watchpoint - new data: %#" PRIxn "\n",
-			    *((unative_t *) breakpoints[slot].address));
+			    *((sysarg_t *) breakpoints[slot].address));
 		}
 	}
@@ -279,5 +279,5 @@
 #endif
 	
-	unative_t dr6 = read_dr6();
+	sysarg_t dr6 = read_dr6();
 	
 	unsigned int i;
@@ -384,5 +384,5 @@
 int cmd_del_breakpoint(cmd_arg_t *argv)
 {
-	unative_t bpno = argv->intval;
+	sysarg_t bpno = argv->intval;
 	if (bpno > BKPOINTS_MAX) {
 		printf("Invalid breakpoint number.\n");
