src/Pure/Tools/proof_general.ML

   val process_pgip: string -> unit
   val tell_clear_goals: unit -> unit
   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
   val init: unit -> unit
   val restart: unit -> unit

 
 
 
 (** 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;
 
 
 (* actions *)