tuned signature -- clarified Proof General legacy;

--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:39:11 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:52:01 2013 +0100
@@ -21,8 +21,6 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     Position.T -> string -> theory list -> theory * (unit -> unit) * int
-  val set_master_path: Path.T -> unit
-  val get_master_path: unit -> Path.T
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -260,16 +258,4 @@
         |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
       end));
 
-
-(* global master path *)  (*Proof General legacy*)
-
-local
-  val master_path = Unsynchronized.ref Path.current;
-in
-
-fun set_master_path path = master_path := path;
-fun get_master_path () = ! master_path;
-
 end;
-
-end;

--- a/src/Pure/Tools/proof_general.ML	Sat Nov 16 17:39:11 2013 +0100
+++ b/src/Pure/Tools/proof_general.ML	Sat Nov 16 17:52:01 2013 +0100
@@ -36,6 +36,7 @@
   val tell_clear_response: unit -> unit
   val inform_file_processed: string -> unit
   val inform_file_retracted: string -> unit
+  val master_path: Path.T Unsynchronized.ref
   structure ThyLoad: sig val add_path: string -> unit end
   val thm_deps: bool Unsynchronized.ref
   val proof_generalN: string
@@ -293,11 +294,14 @@
 
 (** theory loader **)
 
-(* fake old ThyLoad -- with new semantics *)
+(* global master path *)
 
+val master_path = Unsynchronized.ref Path.current;
+
+(*fake old ThyLoad -- with new semantics*)
 structure ThyLoad =
 struct
-  val add_path = Thy_Load.set_master_path o Path.explode;
+  fun add_path path = master_path := Path.explode path;
 end;
 
 

--- a/src/Pure/pure_syn.ML	Sat Nov 16 17:39:11 2013 +0100
+++ b/src/Pure/pure_syn.ML	Sat Nov 16 17:52:01 2013 +0100
@@ -14,7 +14,7 @@
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
+          (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
 
 val _ =
   Outer_Syntax.command