moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -274,10 +274,9 @@
 (* init and exit *)
 
 fun init_theory (name, imports, uses) =
-  Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
-    (fn thy =>
-      if Thy_Info.check_known_thy (Context.theory_name thy)
-      then Thy_Info.end_theory thy else ());
+  Toplevel.init_theory name
+    (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
+    (Theory.end_theory #> tap Thy_Load.check_loaded #> Thy_Info.end_theory);
 
 val exit = Toplevel.keep (fn state =>
  (Context.set_thread_data (try Toplevel.generic_theory_of state);

--- a/src/Pure/Isar/isar_syn.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -304,30 +304,23 @@
 
 (* use ML text *)
 
-fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
-  | propagate_env context = context;
-
-fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
-
 val _ =
   Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.path >>
-      (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
+    (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
 
 val _ =
   Outer_Syntax.command "ML" "ML text within theory or local theory"
     (Keyword.tag_ml Keyword.thy_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+          Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)

--- a/src/Pure/Isar/local_theory.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -5,6 +5,7 @@
 *)
 
 type local_theory = Proof.context;
+type generic_theory = Context.generic;
 
 signature LOCAL_THEORY =
 sig
@@ -25,6 +26,7 @@
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+  val propagate_ml_env: generic_theory -> generic_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
   val global_morphism: local_theory -> morphism
@@ -173,6 +175,10 @@
   target (Context.proof_map f) #>
   Context.proof_map f;
 
+fun propagate_ml_env (context as Context.Proof lthy) =
+      Context.Proof (map_contexts (ML_Env.inherit context) lthy)
+  | propagate_ml_env context = context;
+
 
 (* morphisms *)
 

--- a/src/Pure/Isar/proof.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -17,6 +17,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val map_contexts: (context -> context) -> state -> state
+  val propagate_ml_env: state -> state
   val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
@@ -207,6 +208,9 @@
 
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
+fun propagate_ml_env state = map_contexts
+  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
+
 val bind_terms = map_context o ProofContext.bind_terms;
 val put_thms = map_context oo ProofContext.put_thms;
 

--- a/src/Pure/Isar/toplevel.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -7,7 +7,6 @@
 signature TOPLEVEL =
 sig
   exception UNDEF
-  type generic_theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
@@ -103,8 +102,6 @@
 
 (* local theory wrappers *)
 
-type generic_theory = Context.generic;    (*theory or local_theory*)
-
 val loc_init = Theory_Target.context_cmd;
 val loc_exit = Local_Theory.exit_global;
 

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -137,7 +137,7 @@
     val name = thy_name file;
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
-      if Thy_Info.check_known_thy name then
+      if Thy_Info.known_thy name then
         (Isar.>> (Toplevel.commit_exit Position.none);
             Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
           handle ERROR msg =>

--- a/src/Pure/ROOT.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -184,10 +184,8 @@
 
 (*theory sources*)
 use "Thy/thy_header.ML";
-use "Thy/thy_load.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
-use "Thy/present.ML";
 
 (*basic proof engine*)
 use "Isar/proof_display.ML";
@@ -227,10 +225,12 @@
 use "Isar/constdefs.ML";
 
 (*toplevel transactions*)
+use "Thy/thy_load.ML";
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
 (*theory syntax*)
+use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";

--- a/src/Pure/Thy/thy_info.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -11,7 +11,6 @@
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val known_thy: string -> bool
-  val check_known_thy: string -> bool
   val if_known_thy: (string -> unit) -> string -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
@@ -23,10 +22,6 @@
   val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val provide_file: Path.T -> string -> unit
-  val load_file: Path.T -> unit
-  val exec_file: Path.T -> Context.generic -> Context.generic
-  val use: string -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
@@ -80,18 +75,15 @@
 (* thy database *)
 
 type deps =
-  {update_time: int,                      (*symbolic time of update; negative value means outdated*)
-    master: (Path.T * File.ident) option, (*master dependencies for thy file*)
-    text: string,                         (*source text for thy*)
-    parents: string list,                 (*source specification of parents (partially qualified)*)
-      (*auxiliary files: source path, physical path + identifier*)
-    files: (Path.T * (Path.T * File.ident) option) list};
+ {update_time: int,                      (*symbolic time of update; negative value means outdated*)
+  master: (Path.T * File.ident) option,  (*master dependencies for thy file*)
+  text: string,                          (*source text for thy*)
+  parents: string list};                 (*source specification of parents (partially qualified)*)
 
-fun make_deps update_time master text parents files : deps =
-  {update_time = update_time, master = master, text = text, parents = parents, files = files};
+fun make_deps update_time master text parents : deps =
+  {update_time = update_time, master = master, text = text, parents = parents};
 
-fun init_deps master text parents files =
-  SOME (make_deps ~1 master text parents (map (rpair NONE) files));
+fun init_deps master text parents = SOME (make_deps ~1 master text parents);
 
 fun master_dir NONE = Path.current
   | master_dir (SOME (path, _)) = Path.dir path;
@@ -123,8 +115,7 @@
   SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
 
 val known_thy = is_some o lookup_thy;
-fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
-fun if_known_thy f name = if check_known_thy name then f name else ();
+fun if_known_thy f name = if known_thy name then f name else ();
 
 fun get_thy name =
   (case lookup_thy name of
@@ -144,13 +135,6 @@
 val is_finished = is_none o get_deps;
 val master_directory = master_dir' o get_deps;
 
-fun loaded_files name =
-  (case get_deps name of
-    NONE => []
-  | SOME {master, files, ...} =>
-      (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @
-      (map_filter (Option.map #1 o #2) files));
-
 fun get_parents name =
   thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
     error (loader_msg "nothing known about theory" [name]);
@@ -168,27 +152,16 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
+fun loaded_files name =
+  (case get_deps name of
+    NONE => []
+  | SOME {master, ...} => (case master of SOME (thy_path, _) => [thy_path] | NONE => [])) @
+  Thy_Load.loaded_files (get_theory name);
+
 
 
 (** thy operations **)
 
-(* check state *)
-
-fun check_unfinished fail name =
-  if known_thy name andalso is_finished name then
-    fail (loader_msg "cannot update finished theory" [name])
-  else ();
-
-fun check_files name =
-  let
-    val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
-    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
-    val _ = null missing_files orelse
-      error (loader_msg "unresolved dependencies of theory" [name] ^
-        " on file(s): " ^ commas_quote missing_files);
-  in () end;
-
-
 (* maintain update_time *)
 
 local
@@ -207,8 +180,8 @@
 fun outdate_thy name =
   if is_finished name orelse is_outdated name then ()
   else CRITICAL (fn () =>
-   (change_deps name (Option.map (fn {master, text, parents, files, ...} =>
-    make_deps ~1 master text parents files)); perform Outdate name));
+   (change_deps name (Option.map (fn {master, text, parents, ...} =>
+    make_deps ~1 master text parents)); perform Outdate name));
 
 fun touch_thys names =
   List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
@@ -266,52 +239,6 @@
 val kill_thy = if_known_thy remove_thy;
 
 
-(* load_file *)
-
-local
-
-fun provide path name info (SOME {update_time, master, text, parents, files}) =
-     (if AList.defined (op =) files path then ()
-      else warning (loader_msg "undeclared dependency of theory" [name] ^
-        " on file: " ^ quote (Path.implode path));
-      SOME (make_deps update_time master text parents
-        (AList.update (op =) (path, SOME info) files)))
-  | provide _ _ _ NONE = NONE;
-
-fun run_file path =
-  (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
-    NONE => (Thy_Load.load_ml Path.current path; ())
-  | SOME name =>
-      (case lookup_deps name of
-        SOME deps =>
-          change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
-      | NONE => (Thy_Load.load_ml Path.current path; ())));
-
-in
-
-fun provide_file path name =
-  let
-    val dir = master_directory name;
-    val _ = check_unfinished error name;
-  in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
-
-fun load_file path =
-  if ! Output.timing then
-    let val name = Path.implode path in
-      timeit (fn () =>
-       (priority ("\n**** Starting file " ^ quote name ^ " ****");
-        run_file path;
-        priority ("**** Finished file " ^ quote name ^ " ****\n")))
-    end
-  else run_file path;
-
-fun exec_file path = ML_Context.exec (fn () => load_file path);
-
-val use = load_file o Path.explode;
-
-end;
-
-
 (* load_thy *)
 
 fun required_by _ [] = ""
@@ -321,22 +248,22 @@
   let
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
     fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
-    val (pos, text, _) =
+    val (pos, text) =
       (case get_deps name of
-        SOME {master = SOME (master_path, _), text, files, ...} =>
+        SOME {master = SOME (master_path, _), text, ...} =>
           if text = "" then corrupted ()
-          else (Path.position master_path, text, files)
+          else (Path.position master_path, text)
       | _ => corrupted ());
     val _ = touch_thy name;
     val _ = CRITICAL (fn () =>
-      change_deps name (Option.map (fn {master, text, parents, files, ...} =>
-        make_deps upd_time master text parents files)));
+      change_deps name (Option.map (fn {master, text, parents, ...} =>
+        make_deps upd_time master text parents)));
     val after_load = Outer_Syntax.load_thy name pos text;
     val _ =
       CRITICAL (fn () =>
        (change_deps name
-          (Option.map (fn {update_time, master, parents, files, ...} =>
-            make_deps update_time master "" parents files));
+          (Option.map (fn {update_time, master, parents, ...} =>
+            make_deps update_time master "" parents));
         perform Update name));
   in after_load end;
 
@@ -410,43 +337,33 @@
 
 local
 
-fun check_file master (src_path, info) =
-  let val info' =
-    (case info of
-      NONE => NONE
-    | SOME (_, id) =>
-        (case Thy_Load.test_file (master_dir master) src_path of
-          NONE => NONE
-        | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
-  in (src_path, info') end;
-
 fun check_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
-      in (false, init_deps (SOME master) text parents files, parents) end
-  | SOME (SOME {update_time, master, text, parents, files}) =>
+      let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
+      in (false, init_deps (SOME master) text parents, parents) end
+  | SOME (SOME {update_time, master, text, parents}) =>
       let
         val (thy_path, thy_id) = Thy_Load.check_thy dir name;
         val master' = SOME (thy_path, thy_id);
       in
         if Option.map #2 master <> SOME thy_id then
-          let val {text = text', imports = parents', uses = files', ...} =
-            Thy_Load.deps_thy dir name;
-          in (false, init_deps master' text' parents' files', parents') end
+          let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
+          in (false, init_deps master' text' parents', parents') end
         else
           let
-            val files' = map (check_file master') files;
-            val current = update_time >= 0 andalso can get_theory name
-              andalso forall (is_some o snd) files';
+            val current =
+              (case lookup_theory name of
+                NONE => false
+              | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
             val update_time' = if current then update_time else ~1;
-            val deps' = SOME (make_deps update_time' master' text parents files');
+            val deps' = SOME (make_deps update_time' master' text parents);
           in (current, deps', parents) end
       end);
 
-fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
-  SOME (make_deps update_time master (File.read path) parents files);
+fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
+  SOME (make_deps update_time master (File.read path) parents);
 
 in
 
@@ -495,28 +412,31 @@
   schedule_tasks (snd (require_thys [] dir arg Graph.empty));
 
 val use_thys = use_thys_dir Path.current;
-
-fun use_thy str =
-  let
-    val name = base_name str;
-    val _ = check_unfinished warning name;
-  in use_thys [str] end;
+val use_thy = use_thys o single;
 
 
 (* begin / end theory *)
 
+fun check_unfinished name =
+  if known_thy name andalso is_finished name then
+    error (loader_msg "cannot update finished theory" [name])
+  else ();
+
 fun begin_theory name parents uses int =
   let
     val parent_names = map base_name parents;
     val dir = master_dir'' (lookup_deps name);
-    val _ = check_unfinished error name;
+    val _ = check_unfinished name;
     val _ = if int then use_thys_dir dir parents else ();
 
-    val theory = Theory.begin_theory name (map get_theory parent_names);
+    val theory =
+      Theory.begin_theory name (map get_theory parent_names)
+      |> Thy_Load.init dir
+      |> fold (Thy_Load.require o fst) uses;
 
     val deps =
       if known_thy name then get_deps name
-      else init_deps NONE "" parents (map #1 uses);
+      else init_deps NONE "" parents;
     val _ = change_thys (new_deps name parent_names (deps, NONE));
 
     val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
@@ -527,16 +447,12 @@
 
     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
     val theory'' =
-      fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
+      fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
   in theory'' end;
 
 fun end_theory theory =
-  let
-    val name = Context.theory_name theory;
-    val _ = check_files name;
-    val theory' = Theory.end_theory theory;
-    val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
-  in () end;
+  let val name = Context.theory_name theory
+  in if known_thy name then change_thy name (fn (deps, _) => (deps, SOME theory)) else () end;
 
 
 (* register existing theories *)
@@ -546,14 +462,14 @@
     val _ = priority ("Registering theory " ^ quote name);
     val thy = get_theory name;
     val _ = map get_theory (get_parents name);
-    val _ = check_unfinished error name;
+    val _ = check_unfinished name;
     val _ = touch_thy name;
     val master = #master (Thy_Load.deps_thy Path.current name);
     val upd_time = #2 (Management_Data.get thy);
   in
     CRITICAL (fn () =>
-     (change_deps name (Option.map
-       (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
+     (change_deps name (Option.map (fn {parents, ...} =>
+        make_deps upd_time (SOME master) "" parents));
       perform Update name))
   end;
 

--- a/src/Pure/Thy/thy_load.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -17,6 +17,10 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
+  val master_directory: theory -> Path.T
+  val init: Path.T -> theory -> theory
+  val require: Path.T -> theory -> theory
+  val provide: Path.T * (Path.T * File.ident) -> theory -> theory
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
   val split_thy_path: Path.T -> Path.T * string
@@ -26,12 +30,57 @@
   val check_thy: Path.T -> string -> Path.T * File.ident
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
-  val load_ml: Path.T -> Path.T -> Path.T * File.ident
+  val loaded_files: theory -> Path.T list
+  val check_loaded: theory -> unit
+  val all_current: theory -> bool
+  val provide_file: Path.T -> theory -> theory
+  val use_ml: Path.T -> unit
+  val exec_ml: Path.T -> generic_theory -> generic_theory
 end;
 
 structure Thy_Load: THY_LOAD =
 struct
 
+(* manage source files *)
+
+type files =
+ {master_dir: Path.T,                                 (*master directory of theory source*)
+  required: Path.T list,                              (*source path*)
+  provided: (Path.T * (Path.T * File.ident)) list};   (*source path, physical path, identifier*)
+
+fun make_files (master_dir, required, provided): files =
+ {master_dir = master_dir, required = required, provided = provided};
+
+structure Files = Theory_Data
+(
+  type T = files;
+  val empty = make_files (Path.current, [], []);
+  fun extend _ = empty;
+  fun merge _ = empty;
+);
+
+fun map_files f =
+  Files.map (fn {master_dir, required, provided} =>
+    make_files (f (master_dir, required, provided)));
+
+
+val master_directory = #master_dir o Files.get;
+
+fun init master_dir = map_files (fn _ => (master_dir, [], []));
+
+fun require src_path =
+  map_files (fn (master_dir, required, provided) =>
+    if member (op =) required src_path then
+      error ("Duplicate source file dependency: " ^ Path.implode src_path)
+    else (master_dir, src_path :: required, provided));
+
+fun provide (src_path, path_info) =
+  map_files (fn (master_dir, required, provided) =>
+    if AList.defined (op =) provided src_path then
+      error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
+    else (master_dir, required, (src_path, path_info) :: provided));
+
+
 (* maintain load path *)
 
 local val load_path = Unsynchronized.ref [Path.current] in
@@ -121,13 +170,56 @@
   in {master = master, text = text, imports = imports, uses = uses} end;
 
 
-(* ML files *)
+
+(* loaded files *)
+
+val loaded_files = map (#1 o #2) o #provided o Files.get;
 
-fun load_ml dir raw_path =
+fun check_loaded thy =
+  let
+    val {required, provided, ...} = Files.get thy;
+    val provided_paths = map #1 provided;
+    val _ =
+      (case subtract (op =) provided_paths required of
+        [] => NONE
+      | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad))));
+    val _ =
+      (case subtract (op =) required provided_paths of
+        [] => NONE
+      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad))));
+  in () end;
+
+fun all_current thy =
   let
-    val (path, id) = check_file dir raw_path;
-    val _ = ML_Context.eval_file path;
-  in (path, id) end;
+    val {master_dir, provided, ...} = Files.get thy;
+    fun current (src_path, path_info) =
+      (case test_file master_dir src_path of
+        NONE => false
+      | SOME path_info' => eq_snd (op =) (path_info, path_info'));
+  in can check_loaded thy andalso forall current provided end;
+
+
+(* provide files *)
+
+fun provide_file src_path thy =
+  provide (src_path, check_file (master_directory thy) src_path) thy;
+
+fun use_ml src_path =
+  if is_none (Context.thread_data ()) then
+    ML_Context.eval_file (#1 (check_file Path.current src_path))
+  else
+    let
+      val thy = ML_Context.the_global_context ();
+      val (path, info) = check_file (master_directory thy) src_path;
+
+      val _ = ML_Context.eval_file path;
+      val _ = Context.>> Local_Theory.propagate_ml_env;
+
+      val provide = provide (src_path, (path, info));
+      val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
+    in () end
+
+fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
 
 end;
 

--- a/src/Pure/pure_setup.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/pure_setup.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -51,7 +51,8 @@
 
 (* ML toplevel use commands *)
 
-fun use name = Toplevel.program (fn () => Thy_Info.use name);
+fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
+
 fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
 fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);