# HG changeset patch
# User wenzelm
# Date 1206814456 -3600
# Node ID 6816ca8b48ef5eff7dd822c2b1cd4da99ff20d7e
# Parent  de4764e951664f7fd8d096f2b77d4caf35b10307
added exec_file;
tuned;

diff -r de4764e95166 -r 6816ca8b48ef src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Mar 29 19:14:15 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 29 19:14:16 2008 +0100
@@ -33,6 +33,7 @@
   val touch_child_thys: string -> unit
   val provide_file: Path.T -> string -> unit
   val load_file: bool -> Path.T -> unit
+  val exec_file: bool -> Path.T -> Context.generic -> Context.generic
   val use: string -> unit
   val time_use: string -> unit
   val use_thys: string list -> unit
@@ -308,6 +309,8 @@
     end
   else run_file path;
 
+fun exec_file time path = ML_Context.exec (fn () => load_file time path);
+
 val use = load_file false o Path.explode;
 val time_use = load_file true o Path.explode;
 
@@ -546,8 +549,7 @@
       |> Present.begin_theory update_time dir uses;
 
     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
-    val theory'' =
-      Context.theory_map (ML_Context.exec (fn () => List.app (load_file false) uses_now)) theory';
+    val theory'' = fold (Context.theory_map o exec_file false) uses_now theory';
   in theory'' end;
 
 fun end_theory theory =