Index: kernel/arch/ia32/src/boot/boot.S
===================================================================
--- kernel/arch/ia32/src/boot/boot.S	(revision 6d8c4654bf3953c7eb9e51a4a38c81bb83ee9148)
+++ kernel/arch/ia32/src/boot/boot.S	(revision fb45c7be00697b929cb4f8548767ae72242ce60d)
@@ -125,5 +125,5 @@
 		/* Map kernel and turn paging on */
 		pm_status $status_non_pse
-		call map_kernel
+		call map_kernel_non_pse
 	
 	stack_init:
@@ -196,6 +196,5 @@
  *
  */
-.global map_kernel
-map_kernel:
+map_kernel_non_pse:
 	/* Paging features */
 	movl %cr4, %ecx
Index: kernel/arch/ia32/src/smp/ap.S
===================================================================
--- kernel/arch/ia32/src/smp/ap.S	(revision 6d8c4654bf3953c7eb9e51a4a38c81bb83ee9148)
+++ kernel/arch/ia32/src/smp/ap.S	(revision fb45c7be00697b929cb4f8548767ae72242ce60d)
@@ -74,5 +74,6 @@
 	subl $0x80000000, %esp			# KA2PA(ctx.sp)
 
-	call map_kernel					# map kernel and turn paging on
+	/* We assume that when using SMP, PSE is always available */
+	call map_kernel_pse				# map kernel and turn paging on
 	
 	addl $0x80000000, %esp			# PA2KA(ctx.sp)