diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy
index bfb4949f2..35fcf05e7 100644
--- a/spec/design/m-skel/AARCH64/MachineTypes.thy
+++ b/spec/design/m-skel/AARCH64/MachineTypes.thy
@@ -115,7 +115,8 @@ definition
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 ONLY \
   VMFaultType HypFaultType vmFaultTypeFSR VMPageSize pageBits ptTranslationBits \
   pageBitsForSize \
-  hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR
+  hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR \
+  vcpuBits
 
 end
 
diff --git a/spec/design/skel/AARCH64/Hardware_H.thy b/spec/design/skel/AARCH64/Hardware_H.thy
index 508cc1933..4a174ef6c 100644
--- a/spec/design/skel/AARCH64/Hardware_H.thy
+++ b/spec/design/skel/AARCH64/Hardware_H.thy
@@ -37,7 +37,7 @@ context Arch begin global_naming AARCH64_H
   enableFpuEL01 \
   getFAR getDFSR getIFSR getHSR setHCR getESR  getSCTLR setSCTLR \
   addressTranslateS1 \
-  readVCPUHardwareReg writeVCPUHardwareReg
+  readVCPUHardwareReg writeVCPUHardwareReg vcpuBits
 
 end