clarified signature: master_dir is just Path.current;

--- a/src/Pure/Thy/thy_info.ML	Mon Nov 16 22:28:42 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Nov 16 22:46:02 2020 +0100
@@ -19,7 +19,7 @@
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}
-  val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
+  val use_theories: context -> string -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
@@ -428,13 +428,12 @@
 
 (* use theories *)
 
-fun use_theories context qualifier master_dir imports =
-  let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
+fun use_theories context qualifier imports =
+  let val (_, tasks) = require_thys context [] qualifier Path.current imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
-  use_theories (default_context ()) Resources.default_qualifier
-    Path.current [(name, Position.none)];
+  use_theories (default_context ()) Resources.default_qualifier [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)

--- a/src/Pure/Tools/build.ML	Mon Nov 16 22:28:42 2020 +0100
+++ b/src/Pure/Tools/build.ML	Mon Nov 16 22:46:02 2020 +0100
@@ -55,7 +55,7 @@
 
 (* build theories *)
 
-fun build_theories last_timing qualifier master_dir (options, thys) =
+fun build_theories last_timing qualifier (options, thys) =
   let
     val context = {options = options, last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
@@ -65,7 +65,7 @@
       (Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
-        (Thy_Info.use_theories context qualifier master_dir
+        (Thy_Info.use_theories context qualifier
         |>
           (case Options.string options "profiling" of
             "" => I
@@ -87,22 +87,21 @@
     (fn [args_yxml] =>
         let
           val (html_symbols, (command_timings, (parent_name, (chapter,
-            (session_name, (master_dir, (theories, (session_positions, (session_directories,
+            (session_name, (theories,
+            (session_positions, (session_directories,
             (session_chapters, (doc_names,
-            (global_theories, (loaded_theories, bibtex_entries))))))))))))) =
+            (global_theories, (loaded_theories, bibtex_entries)))))))))))) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
-                val path = Path.explode o string;
               in
                 pair (list (pair string int)) (pair (list properties) (pair string (pair string
-                  (pair string (pair path
-                    (pair (((list (pair Options.decode (list (pair string position))))))
-                      (pair (list (pair string properties)) (pair (list (pair string string))
+                  (pair string (pair (((list (pair Options.decode (list (pair string position))))))
+                    (pair (list (pair string properties)) (pair (list (pair string string))
+                      (pair (list (pair string string)) (pair (list string)
                         (pair (list (pair string string)) (pair (list string)
-                          (pair (list (pair string string)) (pair (list string)
-                            (list (pair string (list string)))))))))))))))
+                          (list (pair string (list string))))))))))))))
               end;
 
           fun build () =
@@ -124,7 +123,7 @@
 
               val res1 =
                 theories |>
-                  (List.app (build_theories last_timing session_name master_dir)
+                  (List.app (build_theories last_timing session_name)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();

--- a/src/Pure/Tools/build.scala	Mon Nov 16 22:28:42 2020 +0100
+++ b/src/Pure/Tools/build.scala	Mon Nov 16 22:46:02 2020 +0100
@@ -175,21 +175,20 @@
             {
               import XML.Encode._
               pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
-                pair(string, pair(Path.encode,
-                pair(list(pair(Options.encode, list(pair(string, properties)))),
+                pair(string, pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(pair(string, string)),
                 pair(list(string),
                 pair(list(pair(string, string)),
-                pair(list(string), list(pair(string, list(string))))))))))))))))(
+                pair(list(string), list(pair(string, list(string)))))))))))))))(
               (Symbol.codes, (command_timings0, (parent, (info.chapter,
-                (session_name, (Path.current, (info.theories,
+                (session_name, (info.theories,
                 (sessions_structure.session_positions,
                 (sessions_structure.dest_session_directories,
                 (sessions_structure.session_chapters,
                 (base.doc_names, (base.global_theories.toList,
-                (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))
+                (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))
             })
 
         val env =