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