diff --git a/include/drivers/timer/exynos4412-mct.h b/include/drivers/timer/exynos4412-mct.h
index fb325ca6c..f62fedcad 100644
--- a/include/drivers/timer/exynos4412-mct.h
+++ b/include/drivers/timer/exynos4412-mct.h
@@ -20,4 +20,45 @@ static inline void resetTimer(void)
     mct_reset();
 }
 
+#ifdef CONFIG_KERNEL_MCS
+/** DONT_TRANSLATE **/
+static inline ticks_t getCurrentTime(void)
+{
+    uint32_t hi, hi2, lo;
+    hi2 = mct->global.cnth;
+
+    do {
+        hi = hi2;
+        lo = mct->global.cntl;
+        hi2 = mct->global.cnth;
+    } while (hi != hi2);
+
+    return ((((uint64_t) hi) << 32llu) | (uint64_t) lo);
+}
+
+/** DONT_TRANSLATE **/
+static inline void setDeadline(ticks_t deadline)
+{
+    /*
+     * After writing a value to a comp register a bit in the wstat
+     * register is asserted. A write of 1 clears this bit.
+     */
+    mct->global.comp0h = (uint32_t)(deadline >> 32u);
+    while (!(mct->global.wstat & GWSTAT_COMP0H));
+    mct->global.wstat |= GWSTAT_COMP0H;
+
+    mct->global.comp0l = (uint32_t) deadline;
+
+    while (!(mct->global.wstat & GWSTAT_COMP0L));
+    mct->global.wstat |= GWSTAT_COMP0L;
+}
+
+static inline void ackDeadlineIRQ(void)
+{
+    /* ack everything */
+    mct_reset();
+}
+
+#endif
+
 #endif /* !__DRIVER_TIMER_MCT_EXYNOS4412_H */
diff --git a/include/drivers/timer/mct.h b/include/drivers/timer/mct.h
index ff8c5d7b0..8157f8502 100644
--- a/include/drivers/timer/mct.h
+++ b/include/drivers/timer/mct.h
@@ -129,46 +129,5 @@ static inline void mct_clear_write_status(void)
     mct->global.cnt_wstat = mct->global.cnt_wstat;
 }
 
-#ifdef CONFIG_KERNEL_MCS
-/** DONT_TRANSLATE **/
-static inline ticks_t getCurrentTime(void)
-{
-    uint32_t hi, hi2, lo;
-    hi2 = mct->global.cnth;
 
-    do {
-        hi = hi2;
-        lo = mct->global.cntl;
-        hi2 = mct->global.cnth;
-    } while (hi != hi2);
-
-    return ((((uint64_t) hi) << 32llu) | (uint64_t) lo);
-}
-
-/** DONT_TRANSLATE **/
-static inline void setDeadline(ticks_t deadline)
-{
-    /*
-     * After writing a value to a comp register a bit in the wstat
-     * register is asserted. A write of 1 clears this bit.
-     */
-    mct->global.comp0h = (uint32_t)(deadline >> 32u);
-    while (!(mct->global.wstat & GWSTAT_COMP0H));
-    mct->global.wstat |= GWSTAT_COMP0H;
-
-    mct->global.comp0l = (uint32_t) deadline;
-
-    while (!(mct->global.wstat & GWSTAT_COMP0L));
-    mct->global.wstat |= GWSTAT_COMP0L;
-}
-
-static inline void ackDeadlineIRQ(void)
-{
-    /* ack everything */
-    mct_reset();
-}
-
-BOOT_CODE void initGenericTimer(void);
-
-#endif
 #endif /* __DRIVERS_TIMER_MCT_H */