diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy
index 106c097d3..2b9020637 100644
--- a/proof/access-control/CNode_AC.thy
+++ b/proof/access-control/CNode_AC.thy
@@ -141,8 +141,6 @@ where
   | CancelBadgedSendsCall cap \<Rightarrow> pas_cap_cur_auth aag cap
   | RevokeCall ptr \<Rightarrow> is_subject aag (fst ptr))"
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma resolve_address_bits_authorised_aux:
   "s \<turnstile> \<lbrace>pas_refined aag and K (is_cnode_cap (fst (cap, cref))
                                \<longrightarrow> (\<forall>x \<in> obj_refs (fst (cap, cref)). is_subject aag x))\<rbrace>
diff --git a/proof/bisim/Separation.thy b/proof/bisim/Separation.thy
index c3a1145d0..0562af96d 100644
--- a/proof/bisim/Separation.thy
+++ b/proof/bisim/Separation.thy
@@ -89,7 +89,7 @@ lemma separate_cnode_cap_rab:
                                                                      (throwError (GuardMismatch (length cref) guard))
                                        | _ \<Rightarrow> throwError InvalidRoot)"
   unfolding separate_cnode_cap_def resolve_address_bits_def
-  by (auto simp: word_bits_def split: cap.split_asm)
+  by (auto simp: word_bits_def resolve_address_bits'.simps split: cap.split_asm)
 
 definition
   "separate_state s \<equiv> \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)"
diff --git a/proof/bisim/Syscall_S.thy b/proof/bisim/Syscall_S.thy
index a75bd5319..0d3c7281f 100644
--- a/proof/bisim/Syscall_S.thy
+++ b/proof/bisim/Syscall_S.thy
@@ -97,6 +97,7 @@ lemma bisim_rab:
                                 | _ \<Rightarrow> throwError undefined
                         odE)
                       (resolve_address_bits (cap, cref))"
+  using resolve_address_bits'.simps[simp]
   unfolding resolve_address_bits_def
   apply (cases "length cref < word_bits")
    apply (auto intro!: bisim_underlyingI
diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy
index 016540b35..f3f2fc61b 100644
--- a/proof/refine/ARM/CSpace1_R.thy
+++ b/proof/refine/ARM/CSpace1_R.thy
@@ -526,8 +526,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma getSlotCap_valid:
   "\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
   getSlotCap p \<lbrace>Q\<rbrace>"
diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy
index 33d89e72c..73800724e 100644
--- a/proof/refine/ARM_HYP/CSpace1_R.thy
+++ b/proof/refine/ARM_HYP/CSpace1_R.thy
@@ -530,8 +530,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma getSlotCap_valid:
   "\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
   getSlotCap p \<lbrace>Q\<rbrace>"
diff --git a/proof/refine/RISCV64/CSpace1_R.thy b/proof/refine/RISCV64/CSpace1_R.thy
index bccd4f722..aa3bd5c9c 100644
--- a/proof/refine/RISCV64/CSpace1_R.thy
+++ b/proof/refine/RISCV64/CSpace1_R.thy
@@ -523,8 +523,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma rab_corres':
   "\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
      bits = length (snd a) \<rbrakk> \<Longrightarrow>
diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy
index 5a66d2b92..27990b4be 100644
--- a/proof/refine/X64/CSpace1_R.thy
+++ b/proof/refine/X64/CSpace1_R.thy
@@ -525,8 +525,6 @@ lemma cap_table_at_gsCNodes:
   apply blast
   done
 
-declare resolve_address_bits'.simps[simp del]
-
 lemma rab_corres':
   "\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
      bits = length (snd a) \<rbrakk> \<Longrightarrow>
diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy
index b1aa4c9eb..9f244968a 100644
--- a/spec/abstract/CSpace_A.thy
+++ b/spec/abstract/CSpace_A.thy
@@ -200,6 +200,8 @@ termination
   apply (auto simp: whenE_def returnOk_def return_def rab_termination)
   done
 
+declare resolve_address_bits'.simps[simp del]
+
 definition resolve_address_bits where
 "resolve_address_bits \<equiv> resolve_address_bits' TYPE('z::state_ext)"