diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy
index 180301a688..32e984889e 100644
--- a/lib/HaskellLib_H.thy
+++ b/lib/HaskellLib_H.thy
@@ -14,8 +14,7 @@ imports
   Lib
   More_Numeral_Type
   Monads.Nondet_VCG
-  Monads.Reader_Option_Monad
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 abbreviation (input) "flip \<equiv> swp"
diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy
index 7d0272dda8..bcc1e310c1 100644
--- a/lib/NonDetMonadLemmaBucket.thy
+++ b/lib/NonDetMonadLemmaBucket.thy
@@ -19,7 +19,7 @@ imports
   Injection_Handler
   Monads.Nondet_While_Loop_Rules_Completeness
   "Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 lemma distinct_tuple_helper:
diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index d6630dc80f..7580326cf6 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -14,7 +14,7 @@ imports
   CParser.LemmaBucket_C
   Lib.LemmaBucket
   SIMPL_Lemmas
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 declare word_neq_0_conv [simp del]
diff --git a/proof/sep-capDL/Lookups_D.thy b/proof/sep-capDL/Lookups_D.thy
index 0fca39865a..1396177f23 100644
--- a/proof/sep-capDL/Lookups_D.thy
+++ b/proof/sep-capDL/Lookups_D.thy
@@ -7,7 +7,7 @@
 theory Lookups_D
 imports
   "DSpec.Syscall_D"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 type_synonym 'a lookup = "cdl_state \<Rightarrow> 'a option"
diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy
index 98c96196f3..7e750b414c 100644
--- a/spec/design/m-skel/AARCH64/MachineTypes.thy
+++ b/spec/design/m-skel/AARCH64/MachineTypes.thy
@@ -9,8 +9,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy
index 6455feb8a4..28613511b3 100644
--- a/spec/design/m-skel/ARM/MachineTypes.thy
+++ b/spec/design/m-skel/ARM/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin
diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
index 7e895ec27b..50d1b6a192 100644
--- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy
+++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin
diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy
index 234e80542c..01ba79fbc3 100644
--- a/spec/design/m-skel/RISCV64/MachineTypes.thy
+++ b/spec/design/m-skel/RISCV64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy
index e8465d4e15..54bb5a930b 100644
--- a/spec/design/m-skel/X64/MachineTypes.thy
+++ b/spec/design/m-skel/X64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy
index 3b54035cad..3f836354cb 100644
--- a/tools/autocorres/NonDetMonadEx.thy
+++ b/tools/autocorres/NonDetMonadEx.thy
@@ -16,7 +16,7 @@ imports
   "Monads.Nondet_More_VCG"
   "Monads.Nondet_No_Throw"
   "Monads.Nondet_No_Fail"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 (*
@@ -276,7 +276,7 @@ lemma whileLoop_to_fold:
            (\<lambda>r. return (Q r))
            i s) = return (if P i \<le> x then fold (\<lambda>i r. (Q r)) [unat (P i) ..< unat x] i else i) s"
     (is "?LHS s = return (?RHS x) s")
-  apply (subst Reader_Option_ND.gets_the_return [symmetric])
+  apply (subst gets_the_return [symmetric])
   apply (subst gets_the_whileLoop)
   apply (rule gets_the_to_return)
   apply (subst owhile_to_fold)
diff --git a/tools/autocorres/TypeStrengthen.thy b/tools/autocorres/TypeStrengthen.thy
index bdebf9aff5..5106ca596c 100644
--- a/tools/autocorres/TypeStrengthen.thy
+++ b/tools/autocorres/TypeStrengthen.thy
@@ -14,7 +14,6 @@
 theory TypeStrengthen
 imports
   L2Defs
-  "Monads.Reader_Option_ND"
   ExecConcrete
 begin