# HG changeset patch
# User wenzelm
# Date 1459944132 -7200
# Node ID 6b2c60ebd915ba483ab0f84b02ab778e08669f44
# Parent  72c475e03e226d0ea240249f49a16f0bd86d3e61
clarified ML bootstrap environment;

diff -r 72c475e03e22 -r 6b2c60ebd915 src/Pure/ML_Bootstrap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML_Bootstrap.thy	Wed Apr 06 14:02:12 2016 +0200
@@ -0,0 +1,35 @@
+(*  Title:      Pure/ML_Bootstrap.thy
+    Author:     Makarius
+
+ML bootstrap environment -- with access to low-level structures!
+*)
+
+theory ML_Bootstrap
+imports Pure
+keywords "use" "use_debug" "use_no_debug" :: thy_load
+begin
+
+setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.command @{command_keyword use}
+    "read and evaluate Isabelle/ML or SML file"
+    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_debug}
+    "read and evaluate Isabelle/ML or SML file (with debugger information)"
+    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_no_debug}
+    "read and evaluate Isabelle/ML or SML file (no debugger information)"
+    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
+
+in end
+\<close>
+
+end
diff -r 72c475e03e22 -r 6b2c60ebd915 src/Pure/ML_Root.thy
--- a/src/Pure/ML_Root.thy	Wed Apr 06 11:57:21 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/ML_Root.thy
-    Author:     Makarius
-
-Support for ML project ROOT file, with imitation of ML "use" commands.
-*)
-
-theory ML_Root
-imports Pure
-keywords "use" "use_debug" "use_no_debug" :: thy_load
-begin
-
-setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
-
-ML \<open>
-local
-
-val _ =
-  Outer_Syntax.command @{command_keyword use}
-    "read and evaluate Isabelle/ML or SML file"
-    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
-
-val _ =
-  Outer_Syntax.command @{command_keyword use_debug}
-    "read and evaluate Isabelle/ML or SML file (with debugger information)"
-    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
-
-val _ =
-  Outer_Syntax.command @{command_keyword use_no_debug}
-    "read and evaluate Isabelle/ML or SML file (no debugger information)"
-    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
-
-in end
-\<close>
-
-end
diff -r 72c475e03e22 -r 6b2c60ebd915 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Apr 06 11:57:21 2016 +0200
+++ b/src/Pure/ROOT	Wed Apr 06 14:02:12 2016 +0200
@@ -4,4 +4,4 @@
   global_theories
     Pure
   theories
-    ML_Root
+    ML_Bootstrap
diff -r 72c475e03e22 -r 6b2c60ebd915 src/Pure/ROOT1.ML
--- a/src/Pure/ROOT1.ML	Wed Apr 06 11:57:21 2016 +0200
+++ b/src/Pure/ROOT1.ML	Wed Apr 06 14:02:12 2016 +0200
@@ -1,6 +1,6 @@
 (*** Isabelle/Pure bootstrap: final setup ***)
 
 use_thy "Pure";
-use_thy "ML_Root";
+use_thy "ML_Bootstrap";
 
 use "ML/ml_pervasive1.ML";