Index: kernel/generic/src/main/kinit.c
===================================================================
--- kernel/generic/src/main/kinit.c	(revision 1cf26abf038d0db4ca5f4e0a43ca1b41d655b01e)
+++ kernel/generic/src/main/kinit.c	(revision 659ebd864ea1645b612057cc3cfc1ca2cfe9c5b6)
@@ -160,5 +160,5 @@
 	 * At this point SMP, if present, is configured.
 	 */
-	arch_post_smp_init();
+	ARCH_OP(post_smp_init);
 	
 	/* Start thread computing system load */
Index: kernel/generic/src/main/main.c
===================================================================
--- kernel/generic/src/main/main.c	(revision 1cf26abf038d0db4ca5f4e0a43ca1b41d655b01e)
+++ kernel/generic/src/main/main.c	(revision 659ebd864ea1645b612057cc3cfc1ca2cfe9c5b6)
@@ -238,5 +238,5 @@
 	 * Memory management subsystems initialization.
 	 */
-	arch_pre_mm_init();
+	ARCH_OP(pre_mm_init);
 	km_identity_init();
 	frame_init();
@@ -250,7 +250,7 @@
 	km_non_identity_init();
 	ddi_init();
-	arch_post_mm_init();
+	ARCH_OP(post_mm_init);
 	reserve_init();
-	arch_pre_smp_init();
+	ARCH_OP(pre_smp_init);
 	smp_init();
 	
@@ -266,5 +266,5 @@
 	cpu_init();
 	calibrate_delay_loop();
-	arch_post_cpu_init();
+	ARCH_OP(post_cpu_init);
 
 	smp_call_init();
@@ -341,13 +341,13 @@
 	the_initialize(THE);
 	
-	arch_pre_mm_init();
+	ARCH_OP(pre_mm_init);
 	frame_init();
 	page_init();
 	tlb_init();
-	arch_post_mm_init();
+	ARCH_OP(post_mm_init);
 	
 	cpu_init();
 	calibrate_delay_loop();
-	arch_post_cpu_init();
+	ARCH_OP(post_cpu_init);
 	
 	the_copy(THE, (the_t *) CPU->stack);