diff --git a/include/arch/arm/arch/32/mode/object/structures.h b/include/arch/arm/arch/32/mode/object/structures.h
index 1478f00d6..4b42228a1 100644
--- a/include/arch/arm/arch/32/mode/object/structures.h
+++ b/include/arch/arm/arch/32/mode/object/structures.h
@@ -99,7 +99,6 @@ typedef struct asid_pool asid_pool_t;
 
 #define HW_ASID_SIZE_BITS 1
 
-#define ASID_POOL_INDEX_BITS seL4_ASIDPoolIndexBits
 #define ASID_BITS (asidHighBits+asidLowBits)
 
 #define nASIDPools BIT(asidHighBits)
@@ -433,4 +432,3 @@ static inline word_t PURE pte_ptr_get_pteType(pte_t *pte_ptr)
     }
 }
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-
diff --git a/include/arch/arm/arch/64/mode/object/structures.h b/include/arch/arm/arch/64/mode/object/structures.h
index d727fe9f2..bdfb25035 100644
--- a/include/arch/arm/arch/64/mode/object/structures.h
+++ b/include/arch/arm/arch/64/mode/object/structures.h
@@ -73,7 +73,6 @@ typedef pte_t pde_t;
 #define ASID_POOL_REF(p)    ((word_t)p)
 
 
-#define ASID_POOL_INDEX_BITS seL4_ASIDPoolIndexBits
 #define ASID_BITS (asidHighBits+asidLowBits)
 #define nASIDs     BIT(ASID_BITS)
 #define nASIDPools BIT(asidHighBits)
diff --git a/include/arch/x86/arch/32/mode/object/structures.h b/include/arch/x86/arch/32/mode/object/structures.h
index 08701ab85..03b234ece 100644
--- a/include/arch/x86/arch/32/mode/object/structures.h
+++ b/include/arch/x86/arch/32/mode/object/structures.h
@@ -51,7 +51,6 @@ struct asid_pool {
 
 typedef struct asid_pool asid_pool_t;
 
-#define ASID_POOL_INDEX_BITS    seL4_ASIDPoolIndexBits
 #define ASID_POOL_PTR(r)    ((asid_pool_t*)r)
 #define ASID_POOL_REF(p)    ((word_t)p)
 #define ASID_BITS           (asidHighBits + asidLowBits)
@@ -116,4 +115,3 @@ static inline void *CONST cap_get_modeCapPtr(cap_t cap)
 {
     fail("Invalid mode cap type");
 }
-
diff --git a/include/arch/x86/arch/64/mode/object/structures.h b/include/arch/x86/arch/64/mode/object/structures.h
index 57d56c2d6..c68dcb9fd 100644
--- a/include/arch/x86/arch/64/mode/object/structures.h
+++ b/include/arch/x86/arch/64/mode/object/structures.h
@@ -102,8 +102,6 @@ struct asid_pool {
 
 typedef struct asid_pool asid_pool_t;
 
-#define ASID_POOL_INDEX_BITS  seL4_ASIDPoolIndexBits
-#define ASID_POOL_SIZE_BITS (seL4_ASIDPoolBits + WORD_SIZE_BITS)
 #define ASID_POOL_PTR(r)    ((asid_pool_t*)r)
 #define ASID_POOL_REF(p)    ((word_t)p)
 #define ASID_BITS           (asidHighBits + asidLowBits)
@@ -192,4 +190,3 @@ static inline void *CONST cap_get_modeCapPtr(cap_t cap)
         return NULL;
     }
 }
-