Index: kernel/arch/mips32/src/drivers/arc.c
===================================================================
--- kernel/arch/mips32/src/drivers/arc.c	(revision 3dea17f5a2dc97de65bf1ff23eb43f3621665af4)
+++ kernel/arch/mips32/src/drivers/arc.c	(revision 1b43a0495c2749ca4430886badcc6e9320843580)
@@ -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 3dea17f5a2dc97de65bf1ff23eb43f3621665af4)
+++ kernel/arch/mips32/src/drivers/serial.c	(revision 1b43a0495c2749ca4430886badcc6e9320843580)
@@ -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 3dea17f5a2dc97de65bf1ff23eb43f3621665af4)
+++ kernel/arch/mips32/src/interrupt.c	(revision 1b43a0495c2749ca4430886badcc6e9320843580)
@@ -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();
 }