--- a/src/Pure/Thy/thy_info.ML Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Jan 19 13:09:33 2007 +0100
@@ -261,7 +261,7 @@
| provide _ _ _ NONE = NONE;
fun run_file path =
- (case Option.map Context.theory_name (Context.get_context ()) of
+ (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
NONE => (ThyLoad.load_file NONE path; ())
| SOME name => (case lookup_deps name of
SOME deps => change_deps name (provide path name
@@ -382,7 +382,7 @@
fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
let val (_, (_, name)) = req [] prfx ([], s)
- in Context.context (get_theory name) end) ();
+ in Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
fun gen_use_thy req = gen_use_thy' req Path.current;
@@ -444,7 +444,9 @@
val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory)));
val theory' = theory |> present dir' name bparents uses;
val _ = put_theory name (Theory.copy theory');
- val ((), theory'') = Context.pass_theory theory' (List.app (load_file false)) uses_now;
+ val ((), theory'') =
+ Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
+ ||> Context.the_theory;
val _ = put_theory name (Theory.copy theory'');
in theory'' end;