diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy
index 5c2ad4add..ab2bfc4f1 100644
--- a/proof/crefine/RISCV64/StateRelation_C.thy
+++ b/proof/crefine/RISCV64/StateRelation_C.thy
@@ -233,7 +233,7 @@ fun
 |   "register_from_H RISCV64.NextIP = scast Kernel_C.NextIP"
 
 definition
-  cregs_relation :: "(MachineTypes.register \<Rightarrow> machine_word) \<Rightarrow> machine_word[35] \<Rightarrow> bool"
+  cregs_relation :: "(MachineTypes.register \<Rightarrow> machine_word) \<Rightarrow> machine_word[registers_count] \<Rightarrow> bool"
 where
   "cregs_relation Hregs Cregs \<equiv>  \<forall>r. Hregs r = Cregs.[unat (register_from_H r)]"
 
diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy
index bcb1c85cb..694c2e534 100644
--- a/proof/crefine/RISCV64/Wellformed_C.thy
+++ b/proof/crefine/RISCV64/Wellformed_C.thy
@@ -39,7 +39,8 @@ abbreviation
   pt_Ptr :: "machine_word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr"
 
 type_synonym tcb_cnode_array = "cte_C[5]"
-type_synonym registers_array = "machine_word[35]"
+type_synonym registers_count = 35
+type_synonym registers_array = "machine_word[registers_count]"
 
 abbreviation "user_context_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_context_C ptr"
 abbreviation "machine_word_Ptr \<equiv> Ptr :: addr \<Rightarrow> machine_word ptr"