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/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