diff --git a/arch/patmos/CMakeLists.txt b/arch/patmos/CMakeLists.txt
index e4de058de8fd43bfab074ae5f887ec9b99e92883..1edbc2d8e8011cade1ada580ace96d3318e336e8 100644
--- a/arch/patmos/CMakeLists.txt
+++ b/arch/patmos/CMakeLists.txt
@@ -14,7 +14,6 @@ set(SRCS
   tcb.cc
   irq.cc
   typecheck.cc
-  platin.cc
   crtend.c
   timing-arch.cc
 )
diff --git a/arch/patmos/platin.cc b/arch/patmos/platin.cc
deleted file mode 100644
index e54a74a8b51f36338f5c710174f7277989b94e03..0000000000000000000000000000000000000000
--- a/arch/patmos/platin.cc
+++ /dev/null
@@ -1,16 +0,0 @@
-#include "os/util/inline.h"
-#include "patmos-cpu.h"
-#include "stdint.h"
-
-
-extern "C" {
-
-inlinehint uint64_t arch_timing_get() {
-    uint32_t l, h;
-    __PATMOS_RTC_RD_CYCLE_LOW(l);
-    __PATMOS_RTC_RD_CYCLE_UP(h);
-
-    return ((uint64_t)h << 32) | l;
-}
-
-}