clarified files;

--- a/src/Pure/ML/ML_Root.thy	Tue Apr 05 21:23:32 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      Pure/ML/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
-  and "use_thy" :: 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));
-
-val _ =
-  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
-    (Parse.path -- @{keyword ";"} >> (fn _ =>
-      Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
-
-in end
-\<close>
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML_Root.thy	Tue Apr 05 21:51:14 2016 +0200
@@ -0,0 +1,41 @@
+(*  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
+  and "use_thy" :: 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));
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
+    (Parse.path -- @{keyword ";"} >> (fn _ =>
+      Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
+
+in end
+\<close>
+
+end

--- a/src/Pure/ROOT	Tue Apr 05 21:23:32 2016 +0200
+++ b/src/Pure/ROOT	Tue Apr 05 21:51:14 2016 +0200
@@ -4,6 +4,6 @@
   global_theories
     Pure
   theories
-    "ML/ML_Root"
+    ML_Root
   files
     "ROOT.ML"

--- a/src/Pure/ROOT.ML	Tue Apr 05 21:23:32 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Apr 05 21:51:14 2016 +0200
@@ -339,4 +339,4 @@
 use_thy "Pure";
 
 use "ML/ml_pervasive_final.ML";
-use_thy "ML/ML_Root";
+use_thy "ML_Root";