diff --git a/proof/ROOT b/proof/ROOT
index d462f6e22..8930d8a58 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -38,14 +38,17 @@ session Refine in "refine" = BaseRefine +
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
   theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
   theories
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
 
 (*
  * This theory is in a separate session because the proofs currently
diff --git a/proof/refine/ARM/ADT_H.thy b/proof/refine/ARM/ADT_H.thy
index 20b379cd0..9c41d7d79 100644
--- a/proof/refine/ARM/ADT_H.thy
+++ b/proof/refine/ARM/ADT_H.thy
@@ -10,7 +10,6 @@ theory ADT_H
 imports
   "AInvs.ADT_AI"
   Syscall_R
-  Init_R
 begin
 
 text \<open>
diff --git a/proof/refine/ARM_HYP/ADT_H.thy b/proof/refine/ARM_HYP/ADT_H.thy
index 5f84cd8e4..01ec349f3 100644
--- a/proof/refine/ARM_HYP/ADT_H.thy
+++ b/proof/refine/ARM_HYP/ADT_H.thy
@@ -10,7 +10,6 @@ theory ADT_H
 imports
   "AInvs.ADT_AI"
   Syscall_R
-  Init_R
 begin
 
 text \<open>
diff --git a/proof/refine/RISCV64/ADT_H.thy b/proof/refine/RISCV64/ADT_H.thy
index 672a69d49..9892819f1 100644
--- a/proof/refine/RISCV64/ADT_H.thy
+++ b/proof/refine/RISCV64/ADT_H.thy
@@ -7,9 +7,7 @@
 chapter \<open>Abstract datatype for the executable specification\<close>
 
 theory ADT_H
-  imports
-    Syscall_R
-    Init_R
+  imports Syscall_R
 begin
 
 text \<open>
diff --git a/proof/refine/X64/ADT_H.thy b/proof/refine/X64/ADT_H.thy
index 1ea1d1640..65d8312c9 100644
--- a/proof/refine/X64/ADT_H.thy
+++ b/proof/refine/X64/ADT_H.thy
@@ -9,7 +9,6 @@ chapter \<open>Abstract datatype for the executable specification\<close>
 theory ADT_H
 imports
   "AInvs.ADT_AI"
-  Init_R
   Syscall_R
 begin