--- a/src/Pure/Thy/thy_info.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Aug 13 20:41:29 2011 +0200
@@ -21,8 +21,7 @@
val use_thys_wrt: Path.T -> string list -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
- val toplevel_begin_theory: Path.T option -> string ->
- string list -> (Path.T * bool) list -> theory
+ val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
val register_thy: theory -> unit
val finish: unit -> unit
end;
@@ -312,9 +311,8 @@
(* toplevel begin theory -- without maintaining database *)
-fun toplevel_begin_theory master name imports uses =
+fun toplevel_begin_theory dir name imports uses =
let
- val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
val _ = kill_thy name;
val _ = use_thys_wrt dir imports;
val parents = map (get_theory o base_name) imports;