# HG changeset patch
# User wenzelm
# Date 1459888288 -7200
# Node ID 3c4161728aa82de6ccfc7568ef1a64e8f61983d3
# Parent  e0b894bba6ff6ffc7c4f4f61e0423f277b074cf3# Parent  20b0cb2f0b87f5a2af360b678035632dc37dfe8f
merged

diff -r e0b894bba6ff -r 3c4161728aa8 NEWS
--- a/NEWS	Tue Apr 05 09:54:17 2016 +0200
+++ b/NEWS	Tue Apr 05 22:31:28 2016 +0200
@@ -235,7 +235,7 @@
 requiring separate files.
 
 * Low-level ML system structures (like PolyML and RunCall) are no longer
-exposed to Isabelle/ML user-space. The system option ML_system_unsafe
+exposed to Isabelle/ML user-space. The system option ML_system_bootstrap
 allows to override this for special test situations.
 
 * Antiquotation @{make_string} is available during Pure bootstrap --
diff -r e0b894bba6ff -r 3c4161728aa8 etc/options
--- a/etc/options	Tue Apr 05 09:54:17 2016 +0200
+++ b/etc/options	Tue Apr 05 22:31:28 2016 +0200
@@ -126,8 +126,8 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
-option ML_system_unsafe : bool = false
-  -- "provide access to low-level ML system structures"
+option ML_system_bootstrap : bool = false
+  -- "provide access to low-level ML system structures (unsafe!)"
 
 
 section "Editor Reactivity"
diff -r e0b894bba6ff -r 3c4161728aa8 lib/scripts/isabelle-platform
--- a/lib/scripts/isabelle-platform	Tue Apr 05 09:54:17 2016 +0200
+++ b/lib/scripts/isabelle-platform	Tue Apr 05 22:31:28 2016 +0200
@@ -4,6 +4,7 @@
 #
 # NOTE: The ML system or JVM may have their own idea about the platform!
 
+ISABELLE_WINDOWS_PREFIX=""
 ISABELLE_PLATFORM_FAMILY=""
 ISABELLE_PLATFORM32=""
 ISABELLE_PLATFORM64=""
@@ -11,6 +12,7 @@
 case $(uname -s) in
   Linux)
     ISABELLE_PLATFORM_FAMILY="linux"
+    ISABELLE_WINDOWS_PREFIX="."
     case $(uname -m) in
       i?86)
         ISABELLE_PLATFORM32=x86-linux
@@ -23,6 +25,7 @@
     ;;
   Darwin)
     ISABELLE_PLATFORM_FAMILY="macos"
+    ISABELLE_WINDOWS_PREFIX="."
     case $(uname -m) in
       i?86)
         ISABELLE_PLATFORM32=x86-darwin
@@ -38,6 +41,7 @@
     ;;
   CYGWIN_NT*)
     ISABELLE_PLATFORM_FAMILY="windows"
+    ISABELLE_WINDOWS_PREFIX="windows"
     case $(uname -m) in
       i?86 | x86_64)
         ISABELLE_PLATFORM32=x86-cygwin
diff -r e0b894bba6ff -r 3c4161728aa8 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Tue Apr 05 22:31:28 2016 +0200
@@ -616,15 +616,15 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
+  @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
   @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
   @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
   @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
-    \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of
+    \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of
     the ML toplevel --- at compile time. ML code needs to take care to refer to
-    @{ML "ML_Context.the_generic_context ()"} correctly. Recall that evaluation
+    @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
     of a function body is delayed until actual run-time.
 
     \<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit
diff -r e0b894bba6ff -r 3c4161728aa8 src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -582,7 +582,7 @@
             case match_aterms varsubst b' a' of
                 NONE => 
                 let
-                    fun mk s = Syntax.string_of_term_global Pure.thy
+                    fun mk s = Syntax.string_of_term_global @{theory Pure}
                       (infer_types (naming_of computer) (encoding_of computer) ty s)
                     val left = "computed left side: "^(mk a')
                     val right = "computed right side: "^(mk b')
diff -r e0b894bba6ff -r 3c4161728aa8 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -280,7 +280,7 @@
                   val output_value = the_default "NONE"
                     (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
                   val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-                    ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
                     |> Context.proof_map (exec false ml_code);
diff -r e0b894bba6ff -r 3c4161728aa8 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Provers/splitter.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -98,9 +98,9 @@
 
 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
 
-val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
-  [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
-  (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
+val lift = Goal.prove_global @{theory Pure} ["P", "Q", "R"]
+  [Syntax.read_prop_global @{theory Pure} "!!x :: 'b. Q(x) == R(x) :: 'c"]
+  (Syntax.read_prop_global @{theory Pure} "P(%x. Q(x)) == P(%x. R(x))")
   (fn {context = ctxt, prems} =>
     rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1)
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/General/symbol.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -119,7 +119,7 @@
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun raw_symbolic s =
-  String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
+  String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
 
 fun is_symbolic s =
   s <> open_ andalso s <> close andalso raw_symbolic s;
@@ -131,7 +131,7 @@
   else is_utf8 s orelse raw_symbolic s;
 
 fun is_control s =
-  String.isPrefix "\<^" s andalso String.isSuffix ">" s;
+  String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
 
 
 (* input source control *)
@@ -142,8 +142,8 @@
 val stopper = Scan.stopper (K eof) is_eof;
 
 fun is_malformed s =
-  String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
-  orelse s = "\<>" orelse s = "\<^>";
+  String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
+  orelse s = "\092<>" orelse s = "\092<^>";
 
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
@@ -201,9 +201,9 @@
 fun encode_raw "" = ""
   | encode_raw str =
       let
-        val raw0 = enclose "\<^raw:" ">";
+        val raw0 = enclose "\092<^raw:" ">";
         val raw1 = raw0 o implode;
-        val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
+        val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;
 
         fun encode cs = enc (take_prefix raw_chr cs)
         and enc ([], []) = []
@@ -233,11 +233,11 @@
 (* decode_raw *)
 
 fun is_raw s =
-  String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
+  String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s;
 
 fun decode_raw s =
   if not (is_raw s) then error (malformed_msg s)
-  else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
+  else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
   else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
 
 
@@ -563,8 +563,8 @@
 
 fun sym_len s =
   if not (is_printable s) then (0: int)
-  else if String.isPrefix "\<long" s then 2
-  else if String.isPrefix "\<Long" s then 2
+  else if String.isPrefix "\092<long" s then 2
+  else if String.isPrefix "\092<Long" s then 2
   else 1;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -515,11 +515,11 @@
   register_config Name_Space.names_long_raw #>
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
+  register_config ML_Print_Depth.print_depth_raw #>
   register_config ML_Options.source_trace_raw #>
   register_config ML_Options.exception_trace_raw #>
   register_config ML_Options.exception_debugger_raw #>
   register_config ML_Options.debugger_raw #>
-  register_config ML_Options.print_depth_raw #>
   register_config Proof_Context.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
   register_config Goal_Display.show_main_goal_raw #>
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -197,8 +197,8 @@
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
     val flags: ML_Compiler.flags =
-      {SML = false, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = false, SML_env = false, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -211,8 +211,8 @@
     val ([{lines, pos, ...}: Token.file], thy') = files thy;
     val source = Input.source true (cat_lines lines) (pos, pos);
     val flags: ML_Compiler.flags =
-      {SML = true, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = true, SML_env = true, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     thy' |> Context.theory_map
       (ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -255,8 +255,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -267,8 +267,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -120,7 +120,7 @@
         NONE => ()
       | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
     val _ =
-      Context_Position.report_generic (ML_Context.the_generic_context ())
+      Context_Position.report_generic (Context.the_generic_context ())
         (command_pos cmd) (command_markup true (name, cmd));
   in Data.map (Symtab.update (name, cmd)) thy end;
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -43,7 +43,7 @@
 fun pretty_exn (exn: exn) =
   Pretty.from_ML
     (ML_Pretty.from_polyml
-      (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+      (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
 
 
 (* exn_context *)
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+    {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
@@ -21,18 +21,19 @@
 (* flags *)
 
 type flags =
-  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+  {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {SML = false, exchange = false, redirect = false, verbose = false,
+  {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
-    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+  {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
+    redirect = #redirect flags, verbose = b, debug = #debug flags,
+    writeln = #writeln flags, warning = #warning flags};
 
 
 (* parse trees *)
@@ -144,7 +145,7 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
+    val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
     val opt_context = Context.thread_data ();
 
 
@@ -153,7 +154,7 @@
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_explode =
-      if #SML flags then String.explode
+      if #SML_syntax flags then String.explode
       else maps (String.explode o Symbol.esc) o Symbol.explode;
 
     val input_buffer =
@@ -198,7 +199,7 @@
 
     (* results *)
 
-    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
+    val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
@@ -257,7 +258,7 @@
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
+      PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
       PolyML.Compiler.CPDebug debug];
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -69,7 +69,7 @@
       | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
             #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
           input line cs (ML_Pretty.make_string_fn "" :: res)
-      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\\\\<" :: res)
+      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res)
       | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
       | input line (c :: cs) res = input line cs (str c :: res)
       | input _ [] res = rev res;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -6,9 +6,6 @@
 
 signature ML_CONTEXT =
 sig
-  val the_generic_context: unit -> Context.generic
-  val the_global_context: unit -> theory
-  val the_local_context: unit -> Proof.context
   val thm: xstring -> thm
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
@@ -35,12 +32,8 @@
 
 (** implicit ML context **)
 
-val the_generic_context = Context.the_thread_data;
-val the_global_context = Context.theory_of o the_generic_context;
-val the_local_context = Context.proof_of o the_generic_context;
-
-fun thm name = Proof_Context.get_thm (the_local_context ()) name;
-fun thms name = Proof_Context.get_thms (the_local_context ()) name;
+fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
+fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
 
 fun exec (e: unit -> unit) context =
   (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
@@ -123,10 +116,10 @@
   (ML_Lex.tokenize
     ("structure " ^ name ^ " =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
-     " (ML_Context.the_local_context ());\n\
+     " (Context.the_local_context ());\n\
      \val ML_print_depth =\n\
-     \  let val default = ML_Options.get_print_depth ()\n\
-     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
+     \  let val default = ML_Print_Depth.get_print_depth ()\n\
+     \  in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
    ML_Lex.tokenize "end;");
 
 fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
@@ -218,7 +211,7 @@
   in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
-  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
+  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_thread_data (Option.map Context.Proof ctxt)
@@ -233,7 +226,7 @@
     eval ML_Compiler.flags (#1 range)
      (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
       ML_Lex.read (": " ^ constraint ^ " =") @ ants @
-      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
+      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
 
 end;
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -12,6 +12,7 @@
   val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
     Context.generic -> Context.generic
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
+  val init_bootstrap: Context.generic -> Context.generic
   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
   val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val context: ML_Compiler0.context
@@ -92,6 +93,23 @@
 
 (* name space *)
 
+val init_bootstrap =
+  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
+    let
+      val sml_tables' =
+        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
+            let
+              val val2 =
+                fold (fn (x, y) =>
+                  member (op =) ML_Name_Space.bootstrap_values x ? Symtab.update (x, y))
+                (#allVal ML_Name_Space.global ()) val1;
+              val structure2 =
+                fold (fn (x, y) =>
+                  member (op =) ML_Name_Space.bootstrap_structures x ? Symtab.update (x, y))
+                (#allStruct ML_Name_Space.global ()) structure1;
+            in (val2, type1, fixity1, structure2, signature1, functor1) end);
+    in make_data (bootstrap, tables, sml_tables', breakpoints) end);
+
 fun add_name_space {SML} (space: ML_Name_Space.T) =
   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     let
@@ -112,7 +130,7 @@
   let
     fun lookup sel1 sel2 name =
       if SML then
-        Context.the_thread_data ()
+        Context.the_generic_context ()
         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
       else
         Context.thread_data ()
@@ -121,7 +139,7 @@
 
     fun all sel1 sel2 () =
       (if SML then
-        Context.the_thread_data ()
+        Context.the_generic_context ()
         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
       else
         Context.thread_data ()
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_file.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -8,7 +8,7 @@
 sig
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
-  val any: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
+  val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure ML_File: ML_FILE =
@@ -19,9 +19,10 @@
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
+    val (SML_syntax, SML_env) = SML src_path;
     val flags =
-      {SML = SML src_path, exchange = false, redirect = true, verbose = true,
-        debug = debug, writeln = writeln, warning = warning};
+      {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
+        verbose = true, debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -29,15 +30,15 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command (K false);
-val SML = command (K true);
+val ML = command (K (false, false));
+val SML = command (K (true, true));
 
-val any =
+val use =
   command (fn path =>
     (case try (#2 o Path.split_ext) path of
-      SOME "ML" => false
-    | SOME "sml" => true
-    | SOME "sig" => true
+      SOME "ML" => (false, true)
+    | SOME "sml" => (true, true)
+    | SOME "sig" => (true, true)
     | _ =>
         error ("Bad file name " ^ Path.print path ^
           "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -58,15 +58,22 @@
   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
 
 
-  (* Standard ML name space *)
+  (* bootstrap environment *)
 
-  val exclude_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+  val bootstrap_values =
+    ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+  val bootstrap_structures =
+    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
 
-  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+
+  (* Standard ML environment *)
+
+  val sml_val =
+    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
   val sml_type = #allType global ();
   val sml_fixity = #allFix global ();
   val sml_structure =
-    List.filter (fn (a, _) => List.all (fn b => a <> b) exclude_structures) (#allStruct global ());
+    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
   val sml_signature = #allSig global ();
   val sml_functor = #allFunct global ();
 end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_options.ML
--- a/src/Pure/ML/ml_options.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_options.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -17,10 +17,6 @@
   val debugger_raw: Config.raw
   val debugger: bool Config.T
   val debugger_enabled: Context.generic option -> bool
-  val print_depth_raw: Config.raw
-  val print_depth: int Config.T
-  val get_print_depth: unit -> int
-  val get_print_depth_default: int -> int
 end;
 
 structure ML_Options: ML_OPTIONS =
@@ -62,21 +58,4 @@
       (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
   | debugger_enabled (SOME context) = Config.get_generic context debugger;
 
-
-(* print depth *)
-
-val print_depth_raw =
-  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ()));
-val print_depth = Config.int print_depth_raw;
-
-fun get_print_depth () =
-  (case Context.thread_data () of
-    NONE => ML_Pretty.get_print_depth ()
-  | SOME context => Config.get_generic context print_depth);
-
-fun get_print_depth_default default =
-  (case Context.thread_data () of
-    NONE => default
-  | SOME context => Config.get_generic context print_depth);
-
 end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_pervasive_final.ML
--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -4,15 +4,14 @@
 Pervasive ML environment: final setup.
 *)
 
-if Options.default_bool "ML_system_unsafe" then ()
+if Options.default_bool "ML_system_bootstrap" then ()
 else
- (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.exclude_structures);
-  ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+  (List.app ML_Name_Space.forget_structure
+    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
-structure Pure = struct val thy = Thy_Info.pure_theory () end;
-
 Proofterm.proofs := 0;
 
 Context.set_thread_data NONE;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -19,8 +19,6 @@
     'a list * FixedInt.int -> pretty
   val to_polyml: pretty -> PolyML_Pretty.pretty
   val from_polyml: PolyML_Pretty.pretty -> pretty
-  val get_print_depth: unit -> int
-  val print_depth: int -> unit
   val format_polyml: int -> PolyML_Pretty.pretty -> string
   val format: int -> pretty -> string
   val make_string_fn: string -> string
@@ -91,16 +89,6 @@
   in convert "" end;
 
 
-(* default print depth *)
-
-local
-  val depth = Unsynchronized.ref 0;
-in
-  fun get_print_depth () = ! depth;
-  fun print_depth n = (depth := n; PolyML.print_depth n);
-end;
-
-
 (* format *)
 
 fun format_polyml margin prt =
@@ -123,8 +111,8 @@
   if local_env <> "" then
     pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
   else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
-    pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
-  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
+    pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()")
+  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
 
 end;
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_print_depth.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,37 @@
+(*  Title:      Pure/ML/ml_print_depth0.ML
+    Author:     Makarius
+
+Print depth for ML toplevel pp: context option with global default.
+*)
+
+signature ML_PRINT_DEPTH =
+sig
+  val set_print_depth: int -> unit
+  val print_depth_raw: Config.raw
+  val print_depth: int Config.T
+  val get_print_depth: unit -> int
+  val get_print_depth_default: int -> int
+end;
+
+structure ML_Print_Depth: ML_PRINT_DEPTH =
+struct
+
+val set_print_depth = ML_Print_Depth.set_print_depth;
+
+val print_depth_raw =
+  Config.declare ("ML_print_depth", @{here})
+    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
+
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+  (case Context.thread_data () of
+    NONE => ML_Print_Depth.get_print_depth ()
+  | SOME context => Config.get_generic context print_depth);
+
+fun get_print_depth_default default =
+  (case Context.thread_data () of
+    NONE => default
+  | SOME context => Config.get_generic context print_depth);
+
+end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_print_depth0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_print_depth0.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Pure/ML/ml_print_depth0.ML
+    Author:     Makarius
+
+Print depth for ML toplevel pp -- global default (unsynchronized).
+*)
+
+signature ML_PRINT_DEPTH =
+sig
+  val set_print_depth: int -> unit
+  val get_print_depth: unit -> int
+  val get_print_depth_default: int -> int
+end;
+
+structure ML_Print_Depth: ML_PRINT_DEPTH =
+struct
+
+val depth = Unsynchronized.ref 0;
+
+fun set_print_depth n = (depth := n; PolyML.print_depth n);
+fun get_print_depth () = ! depth;
+fun get_print_depth_default _ = ! depth;
+
+end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_root.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_root.scala	Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,54 @@
+/*  Title:      Pure/ML/ml_root.scala
+    Author:     Makarius
+
+Support for ML project ROOT file, with imitation of ML "use" commands.
+*/
+
+package isabelle
+
+
+object ML_Root
+{
+  /* parser */
+
+  val ROOT_ML = Path.explode("ROOT.ML")
+
+  val USE = "use"
+  val USE_DEBUG = "use_debug"
+  val USE_NO_DEBUG = "use_no_debug"
+  val USE_THY = "use_thy"
+
+  lazy val syntax =
+    Outer_Syntax.init() + ";" +
+      (USE, Some((Keyword.THY_LOAD, Nil)), None) +
+      (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+      (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+      (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
+
+  private object Parser extends Parse.Parser
+  {
+    val entry: Parser[(String, String)] =
+      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG) | command(USE_THY)) ~!
+        (string ~ $$$(";")) ^^ { case a ~ (b ~ _) => (a, b) }
+
+    def parse(in: Token.Reader): ParseResult[List[(String, String)]] =
+      parse_all(rep(entry), in)
+  }
+
+  def read(dir: Path): List[(String, Path)] =
+  {
+    val root = dir + ROOT_ML
+
+    val toks = Token.explode(syntax.keywords, File.read(root))
+    val start = Token.Pos.file(root.implode)
+
+    Parser.parse(Token.reader(toks, start)) match {
+      case Parser.Success(entries, _) =>
+        for ((a, b) <- entries) yield {
+          val path = dir + Path.explode(b)
+          (a, if (a == USE_THY) Resources.thy_path(path) else path)
+        }
+      case bad => error(bad.toString)
+    }
+  }
+}
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -113,7 +113,7 @@
   fun merge _ = [];
 );
 
-fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
+fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
 val get_stored_thm = hd o get_stored_thms;
 
 fun ml_store get (name, ths) =
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ML_Root.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML_Root.thy	Tue Apr 05 22:31:28 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 ("thy")
+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
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 05 22:31:28 2016 +0200
@@ -101,16 +101,16 @@
 local
 
 val _ =
-  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
+  Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
     (Resources.parse_files "ML_file" >> ML_File.ML NONE);
 
 val _ =
-  Outer_Syntax.command ("ML_file_debug", @{here})
+  Outer_Syntax.command @{command_keyword ML_file_debug}
     "read and evaluate Isabelle/ML file (with debugger information)"
     (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
 
 val _ =
-  Outer_Syntax.command ("ML_file_no_debug", @{here})
+  Outer_Syntax.command @{command_keyword ML_file_no_debug}
     "read and evaluate Isabelle/ML file (no debugger information)"
     (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
 
@@ -133,8 +133,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -145,8 +145,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
-            debug = NONE, writeln = writeln, warning = warning};
+          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
+            verbose = true, debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ROOT	Tue Apr 05 22:31:28 2016 +0200
@@ -1,241 +1,9 @@
 chapter Pure
 
 session Pure =
-  global_theories Pure
+  global_theories
+    Pure
+  theories
+    ML_Root
   files
-    "Concurrent/cache.ML"
-    "Concurrent/counter.ML"
-    "Concurrent/event_timer.ML"
-    "Concurrent/future.ML"
-    "Concurrent/lazy.ML"
-    "Concurrent/mailbox.ML"
-    "Concurrent/multithreading.ML"
-    "Concurrent/par_exn.ML"
-    "Concurrent/par_list.ML"
-    "Concurrent/single_assignment.ML"
-    "Concurrent/standard_thread.ML"
-    "Concurrent/synchronized.ML"
-    "Concurrent/task_queue.ML"
-    "Concurrent/timeout.ML"
-    "Concurrent/unsynchronized.ML"
-    "General/alist.ML"
-    "General/antiquote.ML"
-    "General/balanced_tree.ML"
-    "General/basics.ML"
-    "General/binding.ML"
-    "General/buffer.ML"
-    "General/change_table.ML"
-    "General/completion.ML"
-    "General/exn.ML"
-    "General/file.ML"
-    "General/graph.ML"
-    "General/graph_display.ML"
-    "General/heap.ML"
-    "General/input.ML"
-    "General/integer.ML"
-    "General/linear_set.ML"
-    "General/long_name.ML"
-    "General/name_space.ML"
-    "General/ord_list.ML"
-    "General/output.ML"
-    "General/path.ML"
-    "General/position.ML"
-    "General/pretty.ML"
-    "General/print_mode.ML"
-    "General/properties.ML"
-    "General/queue.ML"
-    "General/random.ML"
-    "General/same.ML"
-    "General/scan.ML"
-    "General/seq.ML"
-    "General/sha1.ML"
-    "General/socket_io.ML"
-    "General/source.ML"
-    "General/stack.ML"
-    "General/symbol.ML"
-    "General/symbol_pos.ML"
-    "General/table.ML"
-    "General/timing.ML"
-    "General/url.ML"
-    "Isar/args.ML"
-    "Isar/attrib.ML"
-    "Isar/auto_bind.ML"
-    "Isar/bundle.ML"
-    "Isar/calculation.ML"
-    "Isar/class.ML"
-    "Isar/class_declaration.ML"
-    "Isar/code.ML"
-    "Isar/context_rules.ML"
-    "Isar/element.ML"
-    "Isar/experiment.ML"
-    "Isar/expression.ML"
-    "Isar/generic_target.ML"
-    "Isar/interpretation.ML"
-    "Isar/isar_cmd.ML"
-    "Isar/keyword.ML"
-    "Isar/local_defs.ML"
-    "Isar/local_theory.ML"
-    "Isar/locale.ML"
-    "Isar/method.ML"
-    "Isar/named_target.ML"
-    "Isar/object_logic.ML"
-    "Isar/obtain.ML"
-    "Isar/outer_syntax.ML"
-    "Isar/overloading.ML"
-    "Isar/parse.ML"
-    "Isar/parse_spec.ML"
-    "Isar/proof.ML"
-    "Isar/proof_context.ML"
-    "Isar/proof_display.ML"
-    "Isar/proof_node.ML"
-    "Isar/rule_cases.ML"
-    "Isar/runtime.ML"
-    "Isar/spec_rules.ML"
-    "Isar/specification.ML"
-    "Isar/subgoal.ML"
-    "Isar/token.ML"
-    "Isar/toplevel.ML"
-    "Isar/typedecl.ML"
-    "ML/exn_debugger.ML"
-    "ML/exn_properties.ML"
-    "ML/ml_antiquotation.ML"
-    "ML/ml_antiquotations.ML"
-    "ML/ml_compiler.ML"
-    "ML/ml_compiler0.ML"
-    "ML/ml_compiler1.ML"
-    "ML/ml_compiler2.ML"
-    "ML/ml_context.ML"
-    "ML/ml_debugger.ML"
-    "ML/ml_env.ML"
-    "ML/ml_file.ML"
-    "ML/ml_heap.ML"
-    "ML/ml_lex.ML"
-    "ML/ml_name_space.ML"
-    "ML/ml_options.ML"
-    "ML/ml_pervasive_final.ML"
-    "ML/ml_pervasive_initial.ML"
-    "ML/ml_pp.ML"
-    "ML/ml_pretty.ML"
-    "ML/ml_profiling.ML"
-    "ML/ml_statistics.ML"
-    "ML/ml_syntax.ML"
-    "ML/ml_system.ML"
-    "ML/ml_thms.ML"
-    "PIDE/active.ML"
-    "PIDE/command.ML"
-    "PIDE/command_span.ML"
-    "PIDE/document.ML"
-    "PIDE/document_id.ML"
-    "PIDE/execution.ML"
-    "PIDE/markup.ML"
-    "PIDE/protocol.ML"
-    "PIDE/protocol_message.ML"
-    "PIDE/query_operation.ML"
-    "PIDE/resources.ML"
-    "PIDE/session.ML"
-    "PIDE/xml.ML"
-    "PIDE/yxml.ML"
-    "Proof/extraction.ML"
-    "Proof/proof_checker.ML"
-    "Proof/proof_rewrite_rules.ML"
-    "Proof/proof_syntax.ML"
-    "Proof/reconstruct.ML"
     "ROOT.ML"
-    "Syntax/ast.ML"
-    "Syntax/lexicon.ML"
-    "Syntax/local_syntax.ML"
-    "Syntax/mixfix.ML"
-    "Syntax/parser.ML"
-    "Syntax/printer.ML"
-    "Syntax/simple_syntax.ML"
-    "Syntax/syntax.ML"
-    "Syntax/syntax_ext.ML"
-    "Syntax/syntax_phases.ML"
-    "Syntax/syntax_trans.ML"
-    "Syntax/term_position.ML"
-    "Syntax/type_annotation.ML"
-    "System/bash.ML"
-    "System/command_line.ML"
-    "System/distribution.ML"
-    "System/invoke_scala.ML"
-    "System/isabelle_process.ML"
-    "System/isabelle_system.ML"
-    "System/message_channel.ML"
-    "System/options.ML"
-    "System/system_channel.ML"
-    "Thy/document_antiquotations.ML"
-    "Thy/html.ML"
-    "Thy/latex.ML"
-    "Thy/markdown.ML"
-    "Thy/present.ML"
-    "Thy/term_style.ML"
-    "Thy/thy_header.ML"
-    "Thy/thy_info.ML"
-    "Thy/thy_output.ML"
-    "Thy/thy_syntax.ML"
-    "Tools/bibtex.ML"
-    "Tools/build.ML"
-    "Tools/class_deps.ML"
-    "Tools/debugger.ML"
-    "Tools/find_consts.ML"
-    "Tools/find_theorems.ML"
-    "Tools/jedit.ML"
-    "Tools/named_theorems.ML"
-    "Tools/named_thms.ML"
-    "Tools/plugin.ML"
-    "Tools/print_operation.ML"
-    "Tools/rail.ML"
-    "Tools/rule_insts.ML"
-    "Tools/simplifier_trace.ML"
-    "Tools/thm_deps.ML"
-    "Tools/thy_deps.ML"
-    "assumption.ML"
-    "axclass.ML"
-    "config.ML"
-    "conjunction.ML"
-    "consts.ML"
-    "context.ML"
-    "context_position.ML"
-    "conv.ML"
-    "defs.ML"
-    "drule.ML"
-    "envir.ML"
-    "facts.ML"
-    "global_theory.ML"
-    "goal.ML"
-    "goal_display.ML"
-    "item_net.ML"
-    "library.ML"
-    "logic.ML"
-    "more_pattern.ML"
-    "more_thm.ML"
-    "more_unify.ML"
-    "morphism.ML"
-    "name.ML"
-    "net.ML"
-    "par_tactical.ML"
-    "pattern.ML"
-    "primitive_defs.ML"
-    "proofterm.ML"
-    "pure_syn.ML"
-    "pure_thy.ML"
-    "raw_simplifier.ML"
-    "search.ML"
-    "sign.ML"
-    "simplifier.ML"
-    "skip_proof.ML"
-    "sorts.ML"
-    "tactic.ML"
-    "tactical.ML"
-    "term.ML"
-    "term_ord.ML"
-    "term_sharing.ML"
-    "term_subst.ML"
-    "term_xml.ML"
-    "theory.ML"
-    "thm.ML"
-    "type.ML"
-    "type_infer.ML"
-    "type_infer_context.ML"
-    "unify.ML"
-    "variable.ML"
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -23,6 +23,7 @@
 
 use "ML/ml_heap.ML";
 use "ML/ml_profiling.ML";
+use "ML/ml_print_depth0.ML";
 use "ML/ml_pretty.ML";
 use "ML/ml_compiler0.ML";
 use_no_debug "ML/ml_debugger.ML";
@@ -185,6 +186,7 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
+use "ML/ml_print_depth.ML";
 use_no_debug "ML/exn_debugger.ML";
 use_no_debug "Isar/runtime.ML";
 use "PIDE/execution.ML";
@@ -226,7 +228,7 @@
 
 
 
-(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
+(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "par_tactical.ML";
@@ -277,7 +279,7 @@
 use "Proof/extraction.ML";
 
 (*Isabelle system*)
-use "System/bash.ML";
+use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
 use "System/isabelle_system.ML";
 
 
@@ -337,3 +339,4 @@
 use_thy "Pure";
 
 use "ML/ml_pervasive_final.ML";
+use_thy "ML_Root";
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/bash.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/bash.ML
     Author:     Makarius
 
-GNU bash processes, with propagation of interrupts.
+GNU bash processes, with propagation of interrupts -- POSIX version.
 *)
 
 signature BASH =
@@ -9,99 +9,6 @@
   val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
 end;
 
-if ML_System.platform_is_windows then ML
-\<open>
-structure Bash: BASH =
-struct
-
-val process = uninterruptible (fn restore_attributes => fn script =>
-  let
-    datatype result = Wait | Signal | Result of int;
-    val result = Synchronized.var "bash_result" Wait;
-
-    val id = serial_string ();
-    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
-    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
-    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
-    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
-
-    fun cleanup_files () =
-     (try File.rm script_path;
-      try File.rm out_path;
-      try File.rm err_path;
-      try File.rm pid_path);
-    val _ = cleanup_files ();
-
-    val system_thread =
-      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
-        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
-          let
-            val _ = File.write script_path script;
-            val bash_script =
-              "bash " ^ File.bash_path script_path ^
-                " > " ^ File.bash_path out_path ^
-                " 2> " ^ File.bash_path err_path;
-            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
-            val rc =
-              Windows.simpleExecute ("",
-                quote (ML_System.platform_path bash_process) ^ " " ^
-                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
-              |> Windows.fromStatus |> SysWord.toInt;
-            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
-          in Synchronized.change result (K res) end
-          handle exn =>
-            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
-
-    fun read_pid 0 = NONE
-      | read_pid count =
-          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
-            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
-          | some => some);
-
-    fun terminate NONE = ()
-      | terminate (SOME pid) =
-          let
-            fun kill s =
-              let
-                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
-                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
-              in
-                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
-                  handle OS.SysErr _ => false
-              end;
-
-            fun multi_kill count s =
-              count = 0 orelse
-                (kill s; kill "0") andalso
-                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
-            val _ =
-              multi_kill 10 "INT" andalso
-              multi_kill 10 "TERM" andalso
-              multi_kill 10 "KILL";
-          in () end;
-
-    fun cleanup () =
-     (Standard_Thread.interrupt_unsynchronized system_thread;
-      cleanup_files ());
-  in
-    let
-      val _ =
-        restore_attributes (fn () =>
-          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
-
-      val out = the_default "" (try File.read out_path);
-      val err = the_default "" (try File.read err_path);
-      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
-      val pid = read_pid 1;
-      val _ = cleanup ();
-    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
-    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
-  end);
-
-end;
-\<close>
-else ML
-\<open>
 structure Bash: BASH =
 struct
 
@@ -192,4 +99,3 @@
   end);
 
 end;
-\<close>;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -209,7 +209,7 @@
 (* init options *)
 
 fun init_options () =
- (ML_Pretty.print_depth (Options.default_int "ML_print_depth");
+ (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   Future.ML_statistics := Options.default_bool "ML_statistics";
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -215,11 +215,13 @@
   | name =>
       let val path = Path.explode name in
         (case try File.read path of
-          SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path))
+          SOME s =>
+            (set_default (decode (YXML.parse_body s));
+             if default_bool "ML_system_bootstrap" then () else ignore (try File.rm path))
         | NONE => ())
       end);
 
 val _ = load_default ();
-val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
+val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
 
 end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/System/windows/bash.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/windows/bash.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -0,0 +1,99 @@
+(*  Title:      Pure/System/windows/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts -- Windows version.
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+  let
+    datatype result = Wait | Signal | Result of int;
+    val result = Synchronized.var "bash_result" Wait;
+
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+    fun cleanup_files () =
+     (try File.rm script_path;
+      try File.rm out_path;
+      try File.rm err_path;
+      try File.rm pid_path);
+    val _ = cleanup_files ();
+
+    val system_thread =
+      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+          let
+            val _ = File.write script_path script;
+            val bash_script =
+              "bash " ^ File.bash_path script_path ^
+                " > " ^ File.bash_path out_path ^
+                " 2> " ^ File.bash_path err_path;
+            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
+            val rc =
+              Windows.simpleExecute ("",
+                quote (ML_System.platform_path bash_process) ^ " " ^
+                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
+              |> Windows.fromStatus |> SysWord.toInt;
+            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
+          in Synchronized.change result (K res) end
+          handle exn =>
+            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
+
+    fun read_pid 0 = NONE
+      | read_pid count =
+          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+          | some => some);
+
+    fun terminate NONE = ()
+      | terminate (SOME pid) =
+          let
+            fun kill s =
+              let
+                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+              in
+                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+                  handle OS.SysErr _ => false
+              end;
+
+            fun multi_kill count s =
+              count = 0 orelse
+                (kill s; kill "0") andalso
+                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+            val _ =
+              multi_kill 10 "INT" andalso
+              multi_kill 10 "TERM" andalso
+              multi_kill 10 "KILL";
+          in () end;
+
+    fun cleanup () =
+     (Standard_Thread.interrupt_unsynchronized system_thread;
+      cleanup_files ());
+  in
+    let
+      val _ =
+        restore_attributes (fn () =>
+          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
+      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val pid = read_pid 1;
+      val _ = cleanup ();
+    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
+  end);
+
+end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 05 22:31:28 2016 +0200
@@ -18,9 +18,6 @@
 {
   /* info */
 
-  val ROOT = Path.explode("ROOT")
-  val ROOTS = Path.explode("ROOTS")
-
   def is_pure(name: String): Boolean = name == "Pure"
 
   sealed case class Info(
@@ -141,6 +138,9 @@
 
   /* parser */
 
+  val ROOT = Path.explode("ROOT")
+  val ROOTS = Path.explode("ROOTS")
+
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
@@ -156,7 +156,7 @@
       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
       IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
 
-  object Parser extends Parse.Parser
+  private object Parser extends Parse.Parser
   {
     private abstract class Entry
     private sealed case class Chapter(name: String) extends Entry
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -260,7 +260,7 @@
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       Resources.load_thy document symbols last_timing update_time dir header text_pos text
-        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
+        (if name = Context.PureN then [Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Apr 05 22:31:28 2016 +0200
@@ -14,6 +14,9 @@
   sealed case class Dep(
     name: Document.Node.Name,
     header: Document.Node.Header)
+  {
+    override def toString: String = name.toString
+  }
 }
 
 class Thy_Info(resources: Resources)
@@ -94,6 +97,8 @@
       val dep_files = Par_List.map(loaded _, rev_deps)
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }
+
+    override def toString: String = deps.toString
   }
 
   private def require_thys(session: String, initiators: List[Document.Node.Name],
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 05 22:31:28 2016 +0200
@@ -173,7 +173,11 @@
             val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
-            val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
+            val loaded_files =
+              if (inlined_files)
+                thy_deps.loaded_files :::
+                  (if (Sessions.is_pure(name)) ML_Root.read(info.dir).map(_._2) else Nil)
+              else Nil
 
             val all_files =
               (theory_files ::: loaded_files :::
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -143,7 +143,7 @@
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {SML = SML, exchange = false, redirect = false, verbose = verbose,
+    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
@@ -155,7 +155,7 @@
 
 fun eval_context thread_name index SML toks =
   let
-    val context = ML_Context.the_generic_context ();
+    val context = Context.the_generic_context ();
     val context1 =
       if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
       then context
@@ -190,7 +190,7 @@
 
     fun print x =
       Pretty.from_polyml
-        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/build-jars	Tue Apr 05 22:31:28 2016 +0200
@@ -54,6 +54,7 @@
   Isar/parse.scala
   Isar/token.scala
   ML/ml_lex.scala
+  ML/ml_root.scala
   ML/ml_syntax.scala
   PIDE/batch_session.scala
   PIDE/command.scala
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/conjunction.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -30,7 +30,7 @@
 
 (** abstract syntax **)
 
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
 val read_prop = certify o Simple_Syntax.read_prop;
 
 val true_prop = certify Logic.true_prop;
@@ -76,7 +76,7 @@
 val A_B = read_prop "A &&& B";
 
 val conjunction_def =
-  Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
+  Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def";
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -137,7 +137,7 @@
 
 local
 
-val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+val bootstrap_thy = Context.the_global_context ();
 
 fun conjs n =
   let
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/context.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -74,9 +74,11 @@
   val proof_of: generic -> Proof.context  (*total*)
   (*thread data*)
   val thread_data: unit -> generic option
-  val the_thread_data: unit -> generic
   val set_thread_data: generic option -> unit
   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
+  val the_generic_context: unit -> generic
+  val the_global_context: unit -> theory
+  val the_local_context: unit -> Proof.context
   val >> : (generic -> generic) -> unit
   val >>> : (generic -> 'a * generic) -> 'a
 end;
@@ -496,19 +498,22 @@
     SOME (SOME context) => SOME context
   | _ => NONE);
 
-fun the_thread_data () =
+fun set_thread_data context = Thread.setLocal (tag, context);
+fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+
+fun the_generic_context () =
   (case thread_data () of
     SOME context => context
   | _ => error "Unknown context");
 
-fun set_thread_data context = Thread.setLocal (tag, context);
-fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+val the_global_context = theory_of o the_generic_context;
+val the_local_context = proof_of o the_generic_context;
 
 end;
 
 fun >>> f =
   let
-    val (res, context') = f (the_thread_data ());
+    val (res, context') = f (the_generic_context ());
     val _ = set_thread_data (SOME context');
   in res end;
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/drule.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -134,7 +134,7 @@
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o Thm.cprop_of;
 
-fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
 
 val implies = certify Logic.implies;
 fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
@@ -570,7 +570,7 @@
 
 local
   val A = certify (Free ("A", propT));
-  val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
+  val axiom = Thm.unvarify_axiom (Context.the_global_context ());
   val prop_def = axiom "Pure.prop_def";
   val term_def = axiom "Pure.term_def";
   val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -645,7 +645,7 @@
   store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
     (Thm.equal_intr
       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
-        (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
+        (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
       (implies_intr_list [A, C] (Thm.assume A)));
 
 end;
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/pure_syn.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -55,7 +55,7 @@
       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
 
-val bootstrap_thy = ML_Context.the_global_context ();
+val bootstrap_thy = Context.the_global_context ();
 
 val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -1392,11 +1392,10 @@
   Variable.gen_all ctxt;
 
 val hhf_ss =
-  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
-    addsimps Drule.norm_hhf_eqs);
+  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
 
 val hhf_protect_ss =
-  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
+  simpset_of (empty_simpset (Context.the_local_context ())
     addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
 
 in
diff -r e0b894bba6ff -r 3c4161728aa8 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -88,7 +88,7 @@
   let
     val code = (prelude
       ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
     val ctxt' = ctxt
       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
       |> Context.proof_map (exec ctxt false code);
@@ -539,7 +539,7 @@
       ML_Compiler0.use_text notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
         (File.read filepath);
-    val thy'' = Context.the_theory (Context.the_thread_data ());
+    val thy'' = Context.the_global_context ();
     val names = Loaded_Values.get thy'';
   in (names, thy'') end;
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Tools/Spec_Check/gen_construction.ML
--- a/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -155,7 +155,7 @@
 
 (*produce compilable string*)
 fun build_check ctxt name (ty, spec) =
-  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+  "Spec_Check.checkGen (Context.the_local_context ()) ("
   ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 
diff -r e0b894bba6ff -r 3c4161728aa8 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 09:54:17 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 22:31:28 2016 +0200
@@ -192,5 +192,5 @@
 
 end;
 
-fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
+fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;