1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:45:49 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 15:50:55 2010 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val loaded_files: string -> Path.T list
     1.5    val remove_thy: string -> unit
     1.6    val kill_thy: string -> unit
     1.7 +  val use_thys_wrt: Path.T -> string list -> unit
     1.8    val use_thys: string list -> unit
     1.9    val use_thy: string -> unit
    1.10    val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
    1.11 @@ -306,10 +307,10 @@
    1.12  
    1.13  (* use_thy *)
    1.14  
    1.15 -fun use_thys_dir dir arg =
    1.16 +fun use_thys_wrt dir arg =
    1.17    schedule_tasks (snd (require_thys [] dir arg Graph.empty));
    1.18  
    1.19 -val use_thys = use_thys_dir Path.current;
    1.20 +val use_thys = use_thys_wrt Path.current;
    1.21  val use_thy = use_thys o single;
    1.22  
    1.23  
    1.24 @@ -319,7 +320,7 @@
    1.25    let
    1.26      val dir = Thy_Load.get_master_path ();
    1.27      val _ = kill_thy name;
    1.28 -    val _ = use_thys_dir dir imports;
    1.29 +    val _ = use_thys_wrt dir imports;
    1.30      val parents = map (get_theory o base_name) imports;
    1.31    in Thy_Load.begin_theory dir name parents uses end;
    1.32