diff --git a/headers/private/kernel/boot/platform/efi/arch_mmu.h b/headers/private/kernel/boot/platform/efi/arch_mmu.h
new file mode 100644
index 0000000000..fadce0d122
--- /dev/null
+++ b/headers/private/kernel/boot/platform/efi/arch_mmu.h
@@ -0,0 +1,10 @@
+/*
+ * Copyright, 2019-2020 Haiku, Inc. All rights reserved.
+ * Distributed under the terms of the MIT License.
+ */
+#ifndef ARCH_MMU_H
+#define ARCH_MMU_H
+
+void arch_mmu_init();
+
+#endif /* ARCH_MMU_H */
diff --git a/src/system/boot/platform/efi/arch/arm/arch_timer.h b/src/system/boot/platform/efi/arch/arm/arch_timer.h
deleted file mode 100644
index bfe3e9b4dd..0000000000
--- a/src/system/boot/platform/efi/arch/arm/arch_timer.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * Copyright 2008, Dustin Howett, dustin.howett@gmail.com. All rights reserved.
- * Distributed under the terms of the MIT License.
- */
-#ifndef HPET_H
-#define HPET_H
-
-#include <SupportDefs.h>
-#include <arch/x86/arch_hpet.h>
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-void arch_timer_init(void);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif	/* HPET_H */
diff --git a/src/system/boot/platform/efi/arch/riscv64/arch_timer.h b/src/system/boot/platform/efi/arch/riscv64/arch_timer.h
deleted file mode 100644
index bfe3e9b4dd..0000000000
--- a/src/system/boot/platform/efi/arch/riscv64/arch_timer.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * Copyright 2008, Dustin Howett, dustin.howett@gmail.com. All rights reserved.
- * Distributed under the terms of the MIT License.
- */
-#ifndef HPET_H
-#define HPET_H
-
-#include <SupportDefs.h>
-#include <arch/x86/arch_hpet.h>
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-void arch_timer_init(void);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif	/* HPET_H */
diff --git a/src/system/boot/platform/efi/arch/x86_64/arch_start.cpp b/src/system/boot/platform/efi/arch/x86_64/arch_start.cpp
index ad1f9984d3..01388634d9 100644
--- a/src/system/boot/platform/efi/arch/x86_64/arch_start.cpp
+++ b/src/system/boot/platform/efi/arch/x86_64/arch_start.cpp
@@ -24,6 +24,15 @@
 extern "C" void arch_enter_kernel(uint64 pml4, uint64 entry_point,
 	uint64 stackTop);
 
+// From arch_mmu.cpp
+extern void arch_mmu_post_efi_setup(size_t memory_map_size,
+    efi_memory_descriptor *memory_map, size_t descriptor_size,
+    uint32_t descriptor_version);
+
+extern uint64_t arch_mmu_generate_post_efi_page_tables(size_t memory_map_size,
+    efi_memory_descriptor *memory_map, size_t descriptor_size,
+    uint32_t descriptor_version);
+
 
 void
 arch_start_kernel(addr_t kernelEntry)
diff --git a/src/system/boot/platform/efi/mmu.h b/src/system/boot/platform/efi/mmu.h
index a222955ae4..a7e5d8311e 100644
--- a/src/system/boot/platform/efi/mmu.h
+++ b/src/system/boot/platform/efi/mmu.h
@@ -47,18 +47,6 @@ extern status_t platform_kernel_address_to_bootloader_address(uint64_t address,
 extern status_t platform_bootloader_address_to_kernel_address(void *address,
 	uint64_t *_result);
 
-// Architecture dependant
-
-extern void arch_mmu_post_efi_setup(size_t memory_map_size,
-    efi_memory_descriptor *memory_map, size_t descriptor_size,
-    uint32_t descriptor_version);
-
-extern uint64_t arch_mmu_generate_post_efi_page_tables(size_t memory_map_size,
-    efi_memory_descriptor *memory_map, size_t descriptor_size,
-    uint32_t descriptor_version);
-
-void arch_mmu_init();
-
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/system/boot/platform/efi/start.cpp b/src/system/boot/platform/efi/start.cpp
index ac4b48d4d5..b420ae037d 100644
--- a/src/system/boot/platform/efi/start.cpp
+++ b/src/system/boot/platform/efi/start.cpp
@@ -19,6 +19,7 @@
 #include <boot/stage2.h>
 #include <boot/stdio.h>
 
+#include "arch_mmu.h"
 #include "arch_start.h"
 #include "acpi.h"
 #include "console.h"