--- a/src/Pure/Thy/thy_info.ML Wed Aug 22 21:06:26 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 22 21:28:33 2012 +0200
@@ -311,14 +311,14 @@
(* toplevel begin theory -- without maintaining database *)
-fun toplevel_begin_theory dir (header: Thy_Header.header) =
+fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
let
val {name, imports, ...} = header;
val _ = kill_thy name;
- val _ = use_thys_wrt dir imports;
+ val _ = use_thys_wrt master_dir imports;
val _ = Thy_Header.define_keywords header;
val parents = map (get_theory o base_name) imports;
- in Thy_Load.begin_theory dir header parents end;
+ in Thy_Load.begin_theory master_dir header parents end;
(* register theory *)