Index: kernel/arch/mips32/include/interrupt.h
===================================================================
--- kernel/arch/mips32/include/interrupt.h	(revision 78595d6da1d919a9ecacafa878d040aaf6b4ce80)
+++ kernel/arch/mips32/include/interrupt.h	(revision b63a7cc2e041ecffd46183cd61923f532c13d113)
@@ -41,5 +41,5 @@
 #define IVT_FIRST 0
 
-extern function timer_fnc;
+extern function virtual_timer_fnc;
 
 extern void interrupt_init(void);
Index: kernel/arch/mips32/src/drivers/arc.c
===================================================================
--- kernel/arch/mips32/src/drivers/arc.c	(revision 78595d6da1d919a9ecacafa878d040aaf6b4ce80)
+++ kernel/arch/mips32/src/drivers/arc.c	(revision b63a7cc2e041ecffd46183cd61923f532c13d113)
@@ -359,5 +359,5 @@
 	
 	chardev_initialize("arc_console", &console, &arc_ops);
-	timer_fnc = &arc_keyboard_poll;
+	virtual_timer_fnc = &arc_keyboard_poll;
 	stdin = &console;
 	stdout = &console;
Index: kernel/arch/mips32/src/drivers/serial.c
===================================================================
--- kernel/arch/mips32/src/drivers/serial.c	(revision 78595d6da1d919a9ecacafa878d040aaf6b4ce80)
+++ kernel/arch/mips32/src/drivers/serial.c	(revision b63a7cc2e041ecffd46183cd61923f532c13d113)
@@ -150,5 +150,5 @@
 	 * don't work on simics
 	 */
-	timer_fnc = &serial_handler;
+	virtual_timer_fnc = &serial_handler;
 	
 	stdin = &console;
Index: kernel/arch/mips32/src/interrupt.c
===================================================================
--- kernel/arch/mips32/src/interrupt.c	(revision 78595d6da1d919a9ecacafa878d040aaf6b4ce80)
+++ kernel/arch/mips32/src/interrupt.c	(revision b63a7cc2e041ecffd46183cd61923f532c13d113)
@@ -47,5 +47,5 @@
 #define TIMER_IRQ 7
 
-function timer_fnc = NULL;
+function virtual_timer_fnc = NULL;
 static irq_t timer_irq;
 
@@ -117,6 +117,6 @@
 	clock();
 	
-	if (timer_fnc != NULL)
-		timer_fnc();
+	if (virtual_timer_fnc != NULL)
+		virtual_timer_fnc();
 }