diff --git a/include/arch/arm/arch/32/mode/object/structures.h b/include/arch/arm/arch/32/mode/object/structures.h
index f6bb938df6a..7e572e5f506 100644
--- a/include/arch/arm/arch/32/mode/object/structures.h
+++ b/include/arch/arm/arch/32/mode/object/structures.h
@@ -42,7 +42,6 @@ typedef pde_t vspace_root_t;
 
 #define PGDE_SIZE_BITS seL4_PGDEntryBits
 #define PDE_SIZE_BITS  seL4_PageDirEntryBits
-#define PTE_SIZE_BITS  seL4_PageTableEntryBits
 #define PGD_INDEX_BITS seL4_PGDIndexBits
 #define PD_INDEX_BITS seL4_PageDirIndexBits
 #define PT_INDEX_BITS seL4_PageTableIndexBits
diff --git a/include/arch/arm/arch/64/mode/object/structures.h b/include/arch/arm/arch/64/mode/object/structures.h
index 781aff1517f..47493bd7267 100644
--- a/include/arch/arm/arch/64/mode/object/structures.h
+++ b/include/arch/arm/arch/64/mode/object/structures.h
@@ -30,7 +30,6 @@ enum vm_rights {
 };
 typedef word_t vm_rights_t;
 
-#define PTE_SIZE_BITS       seL4_PageTableEntryBits
 #define PT_INDEX_BITS       seL4_PageTableIndexBits
 
 #define PT_INDEX_OFFSET     (seL4_PageBits)
diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c
index 4f57027c0fb..fbf6b59e541 100644
--- a/src/arch/arm/32/kernel/vspace.c
+++ b/src/arch/arm/32/kernel/vspace.c
@@ -40,7 +40,7 @@
 
 /* helper stuff to avoid fencepost errors when
  * getting the last byte of a PTE or PDE */
-#define LAST_BYTE_PTE(PTE,LENGTH) ((word_t)&(PTE)[(LENGTH)-1] + (BIT(PTE_SIZE_BITS)-1))
+#define LAST_BYTE_PTE(PTE,LENGTH) ((word_t)&(PTE)[(LENGTH)-1] + (BIT(seL4_PageTableEntryBits)-1))
 #define LAST_BYTE_PDE(PDE,LENGTH) ((word_t)&(PDE)[(LENGTH)-1] + (BIT(PDE_SIZE_BITS)-1))
 
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
diff --git a/src/arch/arm/32/object/objecttype.c b/src/arch/arm/32/object/objecttype.c
index 87337b206e8..902420526d4 100644
--- a/src/arch/arm/32/object/objecttype.c
+++ b/src/arch/arm/32/object/objecttype.c
@@ -359,7 +359,7 @@ word_t Arch_getObjectSize(word_t t)
     case seL4_ARM_SuperSectionObject:
         return ARMSuperSectionBits;
     case seL4_ARM_PageTableObject:
-        return PTE_SIZE_BITS + PT_INDEX_BITS;
+        return seL4_PageTableEntryBits + PT_INDEX_BITS;
     case seL4_ARM_PageDirectoryObject:
         return PDE_SIZE_BITS + PD_INDEX_BITS;
 #ifdef CONFIG_TK1_SMMU