--- a/src/Pure/Thy/thy_info.ML Thu Mar 27 21:49:10 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Mar 28 00:02:54 2008 +0100
@@ -546,9 +546,8 @@
|> Present.begin_theory update_time dir uses;
val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
- val ((), theory'') =
- ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
- ||> Context.the_theory;
+ val theory'' =
+ Context.theory_map (ML_Context.exec (fn () => List.app (load_file false) uses_now)) theory';
in theory'' end;
fun end_theory theory =