diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy
index 15b994746a..e74e29273c 100644
--- a/proof/crefine/AARCH64/Invoke_C.thy
+++ b/proof/crefine/AARCH64/Invoke_C.thy
@@ -2812,10 +2812,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)
diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy
index 20481e5bd0..ba8b9a0df9 100644
--- a/proof/crefine/AARCH64/Retype_C.thy
+++ b/proof/crefine/AARCH64/Retype_C.thy
@@ -5047,7 +5047,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -5070,14 +5070,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory
diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy
index 9cccf1178e..524f811aeb 100644
--- a/proof/crefine/ARM/Invoke_C.thy
+++ b/proof/crefine/ARM/Invoke_C.thy
@@ -2623,10 +2623,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)
diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy
index f72ef05c28..b0b5fd33ec 100644
--- a/proof/crefine/ARM/Retype_C.thy
+++ b/proof/crefine/ARM/Retype_C.thy
@@ -4350,7 +4350,7 @@ lemma placeNewObject_user_data:
 
 
 definition
-  createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4373,14 +4373,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory
diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy
index 103d13b238..84432c6231 100644
--- a/proof/crefine/ARM_HYP/Invoke_C.thy
+++ b/proof/crefine/ARM_HYP/Invoke_C.thy
@@ -2828,10 +2828,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)
diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
index be5ff3990e..a6762ccc4e 100644
--- a/proof/crefine/ARM_HYP/Retype_C.thy
+++ b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -4919,7 +4919,7 @@ lemma placeNewObject_user_data:
 
 
 definition
-  createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4942,14 +4942,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory
diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy
index f74814a574..b521bd42b2 100644
--- a/proof/crefine/RISCV64/Invoke_C.thy
+++ b/proof/crefine/RISCV64/Invoke_C.thy
@@ -2774,10 +2774,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)
diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy
index 77d931c5e0..539221b01c 100644
--- a/proof/crefine/RISCV64/Retype_C.thy
+++ b/proof/crefine/RISCV64/Retype_C.thy
@@ -4796,7 +4796,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4819,14 +4819,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory
diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy
index 3c24ca6970..9b94f45d7a 100644
--- a/proof/crefine/X64/Invoke_C.thy
+++ b/proof/crefine/X64/Invoke_C.thy
@@ -2800,10 +2800,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)
diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy
index f2963a8ff8..122be6b735 100644
--- a/proof/crefine/X64/Retype_C.thy
+++ b/proof/crefine/X64/Retype_C.thy
@@ -5628,7 +5628,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -5651,14 +5651,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory
diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy
index 79466cd0cc..8a5061f324 100644
--- a/proof/refine/AARCH64/Syscall_R.thy
+++ b/proof/refine/AARCH64/Syscall_R.thy
@@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"
diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy
index 422530076f..1b6188b32e 100644
--- a/proof/refine/ARM/Syscall_R.thy
+++ b/proof/refine/ARM/Syscall_R.thy
@@ -526,7 +526,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"
diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy
index 60d9e6ba12..efe187dda3 100644
--- a/proof/refine/ARM/orphanage/Orphanage.thy
+++ b/proof/refine/ARM/orphanage/Orphanage.thy
@@ -1797,11 +1797,11 @@ lemma invokeIRQControl_no_orphans [wp]:
   apply (wp | clarsimp)+
   done
 
-lemma invokeIRQHandler_no_orphans [wp]:
+lemma arch_invokeIRQHandler_no_orphans[wp]:
   "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
-   invokeIRQHandler i
+   ARM_H.invokeIRQHandler i
    \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>"
-  apply (cases i, simp_all add: invokeIRQHandler_def)
+  apply (cases i, simp_all add: ARM_H.invokeIRQHandler_def)
     apply (wp | clarsimp | fastforce)+
   done
 
@@ -1939,7 +1939,7 @@ lemma setDomain_no_orphans [wp]:
   apply (fastforce simp: tcb_at_typ_at'  is_active_tcb_ptr_runnable')
   done
 
-crunch InterruptDecls_H.invokeIRQHandler
+crunch invokeIRQHandler
   for no_orphans[wp]: no_orphans
 
 lemma performInvocation_no_orphans [wp]:
diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy
index 52873b90a3..80a53138fd 100644
--- a/proof/refine/ARM_HYP/Syscall_R.thy
+++ b/proof/refine/ARM_HYP/Syscall_R.thy
@@ -536,7 +536,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"
diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy
index 63b7ff5d2f..892fc1034d 100644
--- a/proof/refine/RISCV64/Syscall_R.thy
+++ b/proof/refine/RISCV64/Syscall_R.thy
@@ -534,7 +534,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"
diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy
index cd9575f6a9..4db9157811 100644
--- a/proof/refine/X64/Syscall_R.thy
+++ b/proof/refine/X64/Syscall_R.thy
@@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"