diff --git a/repos/base-hw/lib/mk/x86_64/core.mk b/repos/base-hw/lib/mk/x86_64/core.mk
index db26ef3cf..f678091a5 100644
--- a/repos/base-hw/lib/mk/x86_64/core.mk
+++ b/repos/base-hw/lib/mk/x86_64/core.mk
@@ -17,6 +17,7 @@ SRC_S += spec/x86_64/crt0.s
 # add C++ sources
 SRC_CC += spec/x86/pic.cc
 SRC_CC += spec/x86_64/kernel/thread_base.cc
+SRC_CC += spec/x86_64/platform_support.cc
 SRC_CC += spec/x86_64/idt.cc
 SRC_CC += spec/x86_64/tss.cc
 
diff --git a/repos/base-hw/src/core/spec/x86/platform_support.cc b/repos/base-hw/src/core/spec/x86/platform_support.cc
index c84535d65..6a8106d09 100644
--- a/repos/base-hw/src/core/spec/x86/platform_support.cc
+++ b/repos/base-hw/src/core/spec/x86/platform_support.cc
@@ -33,17 +33,6 @@ Native_region * Platform::_ram_regions(unsigned const i)
 }
 
 
-Native_region * Platform::_core_only_mmio_regions(unsigned const i)
-{
-	static Native_region _regions[] =
-	{
-		{ Board::MMIO_LAPIC_BASE,  Board::MMIO_LAPIC_SIZE  },
-		{ Board::MMIO_IOAPIC_BASE, Board::MMIO_IOAPIC_SIZE },
-	};
-	return i < sizeof(_regions)/sizeof(_regions[0]) ? &_regions[i] : 0;
-}
-
-
 void Platform::_init_io_port_alloc()
 {
 	_io_port_alloc.add_range(0, 0x10000);
diff --git a/repos/base-hw/src/core/spec/x86_64/platform_support.cc b/repos/base-hw/src/core/spec/x86_64/platform_support.cc
new file mode 100644
index 000000000..3d842e5b6
--- /dev/null
+++ b/repos/base-hw/src/core/spec/x86_64/platform_support.cc
@@ -0,0 +1,28 @@
+/*
+ * \brief   Platform implementations specific for x86_64
+ * \author  Reto Buerki
+ * \date    2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* core includes */
+#include <platform.h>
+#include <board.h>
+
+using namespace Genode;
+
+Native_region * Platform::_core_only_mmio_regions(unsigned const i)
+{
+	static Native_region _regions[] =
+	{
+		{ Board::MMIO_LAPIC_BASE,  Board::MMIO_LAPIC_SIZE  },
+		{ Board::MMIO_IOAPIC_BASE, Board::MMIO_IOAPIC_SIZE },
+	};
+	return i < sizeof(_regions)/sizeof(_regions[0]) ? &_regions[i] : 0;
+}