diff --git a/src/kernel/core/arch/ppc/arch_cpu.c b/src/kernel/core/arch/ppc/arch_cpu.c
index f240dd8d7d..c4e649c724 100755
--- a/src/kernel/core/arch/ppc/arch_cpu.c
+++ b/src/kernel/core/arch/ppc/arch_cpu.c
@@ -109,8 +109,7 @@ arch_cpu_global_TLB_invalidate(void)
 
 
 // ToDo: doesn't belong here!
-#include <OS.h>
-
+#if 0
 long long 
 system_time(void)
 {
@@ -119,6 +118,7 @@ system_time(void)
 	return (time_base * 1000000) / ((66*1000*1000) / 4); 
 		// ToDo: remove hard coded
 }
+#endif
 
 
 int