diff --git a/kernel/src/api/v4/tcb.h b/kernel/src/api/v4/tcb.h
index 95bc8c17..8288cdf4 100644
--- a/kernel/src/api/v4/tcb.h
+++ b/kernel/src/api/v4/tcb.h
@@ -191,11 +191,7 @@ public:
 
     /* utcb access functions */
     utcb_t * get_utcb()
-#ifdef CONFIG_ARCH_ARM
-        ;
-#else
         const { return this->utcb; }
-#endif
 
 public:
     void set_scheduler(const threadid_t tid);