diff --git a/grub-core/kern/i386/tsc.c b/grub-core/kern/i386/tsc.c
index d7d1783e4..bc441d0d3 100644
--- a/grub-core/kern/i386/tsc.c
+++ b/grub-core/kern/i386/tsc.c
@@ -57,6 +57,8 @@ grub_get_tsc (void)
   return (((grub_uint64_t) hi) << 32) | lo;
 }
 
+#ifndef GRUB_MACHINE_XEN
+
 static __inline int
 grub_cpu_is_tsc_supported (void)
 {
@@ -69,8 +71,6 @@ grub_cpu_is_tsc_supported (void)
   return (d & (1 << 4)) != 0;
 }
 
-#ifndef GRUB_MACHINE_XEN
-
 static void
 grub_pit_wait (grub_uint16_t tics)
 {