Index: kernel/arch/mips64/src/mips64.c
===================================================================
--- kernel/arch/mips64/src/mips64.c	(revision 232cd4f80cf97c780667bf57b298508cd538ea7b)
+++ kernel/arch/mips64/src/mips64.c	(revision d5b9e8d0db718c208ae5e80f1ed56e9201df1a55)
@@ -46,5 +46,7 @@
 #include <arch/debug.h>
 #include <arch/debugger.h>
+#ifdef MACHINE_msim
 #include <arch/drivers/msim.h>
+#endif
 #include <genarch/fb/fb.h>
 #include <genarch/drivers/dsrln/dsrlnin.h>
@@ -125,5 +127,5 @@
 	interrupt_init();
 	
-#ifdef CONFIG_MIPS_PRN
+#ifdef CONFIG_MSIM_PRN
 	outdev_t *dsrlndev = dsrlnout_init((ioport8_t *) MSIM_KBD_ADDRESS);
 	if (dsrlndev)
@@ -151,5 +153,5 @@
 	    str_size(platform));
 	
-#ifdef CONFIG_MIPS_KBD
+#ifdef CONFIG_MSIM_KBD
 	/*
 	 * Initialize the msim keyboard port. Then initialize the serial line
Index: kernel/arch/mips64/src/mm/frame.c
===================================================================
--- kernel/arch/mips64/src/mm/frame.c	(revision 232cd4f80cf97c780667bf57b298508cd538ea7b)
+++ kernel/arch/mips64/src/mm/frame.c	(revision d5b9e8d0db718c208ae5e80f1ed56e9201df1a55)
@@ -40,5 +40,7 @@
 #include <mm/asid.h>
 #include <config.h>
+#ifdef MACHINE_msim
 #include <arch/drivers/msim.h>
+#endif
 #include <print.h>