lib+tools: MLUtils -> ML_Utils for consistency

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Apply_Trace.thy

@@ -8,7 +8,7 @@
  * Provides an alternate refinement function which takes an additional stateful journaling operation. *)
 theory Apply_Trace
 imports
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
 begin
 
 

lib/Crunch.thy

@@ -8,7 +8,7 @@ theory Crunch
 imports
   WPSimp
   Lib
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
 keywords "crunch" "crunch_ignore" "crunches" :: thy_decl
 begin
 

lib/ML_Goal_Test.thy

@@ -7,7 +7,7 @@
 theory ML_Goal_Test
 imports
   ML_Goal
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
 begin
 experiment begin
 

lib/ML_Utils/ML_Utils.thy

@@ -5,7 +5,7 @@
  *)
 
 \<comment>\<open>
-  MLUtils is a collection of 'basic' ML utilities (kind of like @{file
+  ML_Utils is a collection of 'basic' ML utilities (kind of like @{file
   "~~/src/Pure/library.ML"}, but maintained by Trustworthy Systems). If you
   find yourself implementing:
       - A simple data-structure-shuffling task,
@@ -16,7 +16,7 @@
   consider adding it here.
 \<close>
 
-theory MLUtils
+theory ML_Utils
 imports Main
 begin
 ML_file "StringExtras.ML"

lib/ML_Utils/ROOT

@@ -8,7 +8,7 @@ chapter Lib
 
 session ML_Utils (lib) = HOL +
   theories
-    MLUtils
+    ML_Utils
     MkTermAntiquote
     TermPatternAntiquote
     TacticAntiquotation

lib/Monad_WP/Datatype_Schematic.thy

@@ -6,7 +6,7 @@
 theory Datatype_Schematic
 
 imports
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
   ML_Utils.TermPatternAntiquote
 begin
 

lib/Monad_WP/wp/WP.thy

@@ -9,7 +9,7 @@ imports
   WP_Pre
   WPFix
   Apply_Debug
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
 begin
 
 definition

lib/Trace_Schematic_Insts.thy

@@ -6,7 +6,7 @@
 
 theory Trace_Schematic_Insts
 imports
-  ML_Utils.MLUtils
+  ML_Utils.ML_Utils
   ML_Utils.TermPatternAntiquote
 begin
 

tools/c-parser/CTranslation.thy

@@ -11,7 +11,7 @@ imports
   "StaticFun"
   "IndirectCalls"
   "ModifiesProofs"
-  "ML_Utils.MLUtils"
+  "ML_Utils.ML_Utils"
   "HOL-Eisbach.Eisbach"
 keywords
   "cond_sorry_modifies_proofs"

tools/c-parser/mkrelease

@@ -127,7 +127,7 @@ cat > "$outputdir/src/lib/ROOT" <<EOF
 
 session Lib = HOL +
   directories "ml-helpers"
-  theories "MLUtils"
+  theories "ML_Utils"
 EOF
 
 echo "Rearranging directories"