clarified implicit Pure.thy;

--- a/src/Pure/ML/ml_pp.ML	Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/ML/ml_pp.ML	Mon Jan 08 22:36:02 2018 +0100
@@ -12,19 +12,19 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure);
 
 val _ =
   ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);
 
 
 local

--- a/src/Pure/PIDE/document.ML	Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Jan 08 22:36:02 2018 +0100
@@ -574,7 +574,7 @@
         |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
 
     val parents =
-      if null parents_reports then [Thy_Info.pure_theory ()] else map #1 parents_reports;
+      if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 

--- a/src/Pure/Thy/thy_info.ML	Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Jan 08 22:36:02 2018 +0100
@@ -10,7 +10,6 @@
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
-  val pure_theory: unit -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
@@ -102,8 +101,6 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
-fun pure_theory () = get_theory Context.PureN;
-
 val get_imports = Resources.imports_of o get_theory;
 
 

--- a/src/Pure/Tools/build.scala	Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 08 22:36:02 2018 +0100
@@ -265,7 +265,8 @@
           val eval =
             "Command_Line.tool0 (fn () => (" +
             "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
-            (if (do_output) "; " + save_heap else "") + "));"
+            (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)"
+             else "") + (if (do_output) "; " + save_heap else "") + "));"
 
           val process =
             if (Sessions.is_pure(name)) {

--- a/src/Pure/theory.ML	Mon Jan 08 16:45:30 2018 +0100
+++ b/src/Pure/theory.ML	Mon Jan 08 22:36:02 2018 +0100
@@ -11,6 +11,8 @@
   val nodes_of: theory -> theory list
   val setup: (theory -> theory) -> unit
   val local_setup: (Proof.context -> Proof.context) -> unit
+  val get_pure: unit -> theory
+  val install_pure: theory -> unit
   val get_markup: theory -> Markup.T
   val check: Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
@@ -45,6 +47,10 @@
 fun setup f = Context.>> (Context.map_theory f);
 fun local_setup f = Context.>> (Context.map_proof f);
 
+val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
+fun get_pure () = the (Single_Assignment.peek pure);
+fun install_pure thy = Single_Assignment.assign pure thy;
+
 
 
 (** datatype thy **)