Index: kernel/arch/arm32/include/mm/page.h
===================================================================
--- kernel/arch/arm32/include/mm/page.h	(revision 97c76825acca82d15cb8daa0e50df4f66ffd6c0b)
+++ kernel/arch/arm32/include/mm/page.h	(revision 804d9b62fe9ebfd0dbe04bdf00f0bd0114431bfe)
@@ -135,24 +135,4 @@
 #endif
 
-#ifndef __ASM__
-NO_TRACE static inline void set_pt_level0_present(pte_t *pt, size_t i)
-{
-	pte_level0_t *p = &pt[i].l0;
-
-	p->should_be_zero = 0;
-	write_barrier();
-	p->descriptor_type = PTE_DESCRIPTOR_COARSE_TABLE;
-}
-
-
-NO_TRACE static inline void set_pt_level1_present(pte_t *pt, size_t i)
-{
-	pte_level1_t *p = &pt[i].l1;
-
-	p->descriptor_type = PTE_DESCRIPTOR_SMALL_PAGE;
-}
-
-#endif /* __ASM__ */
-
 #endif
 
Index: kernel/arch/arm32/include/mm/page_armv4.h
===================================================================
--- kernel/arch/arm32/include/mm/page_armv4.h	(revision 97c76825acca82d15cb8daa0e50df4f66ffd6c0b)
+++ kernel/arch/arm32/include/mm/page_armv4.h	(revision 804d9b62fe9ebfd0dbe04bdf00f0bd0114431bfe)
@@ -241,4 +241,21 @@
 }
 
+NO_TRACE static inline void set_pt_level0_present(pte_t *pt, size_t i)
+{
+	pte_level0_t *p = &pt[i].l0;
+
+	p->should_be_zero = 0;
+	write_barrier();
+	p->descriptor_type = PTE_DESCRIPTOR_COARSE_TABLE;
+}
+
+
+NO_TRACE static inline void set_pt_level1_present(pte_t *pt, size_t i)
+{
+	pte_level1_t *p = &pt[i].l1;
+
+	p->descriptor_type = PTE_DESCRIPTOR_SMALL_PAGE;
+}
+
 
 extern void page_arch_init(void);
Index: kernel/arch/arm32/include/mm/page_armv7.h
===================================================================
--- kernel/arch/arm32/include/mm/page_armv7.h	(revision 97c76825acca82d15cb8daa0e50df4f66ffd6c0b)
+++ kernel/arch/arm32/include/mm/page_armv7.h	(revision 804d9b62fe9ebfd0dbe04bdf00f0bd0114431bfe)
@@ -258,4 +258,21 @@
 }
 
+NO_TRACE static inline void set_pt_level0_present(pte_t *pt, size_t i)
+{
+	pte_level0_t *p = &pt[i].l0;
+
+	p->should_be_zero_0 = 0;
+	p->should_be_zero_1 = 0;
+	write_barrier();
+	p->descriptor_type = PTE_DESCRIPTOR_COARSE_TABLE;
+}
+
+NO_TRACE static inline void set_pt_level1_present(pte_t *pt, size_t i)
+{
+	pte_level1_t *p = &pt[i].l1;
+
+	p->descriptor_type = PTE_DESCRIPTOR_SMALL_PAGE;
+}
+
 
 extern void page_arch_init(void);