--- a/src/Pure/Isar/isar_thy.ML Wed Oct 27 17:25:36 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Wed Oct 27 17:25:53 1999 +0200
@@ -158,6 +158,7 @@
val kill_theory: string -> unit
val theory: string * string list * (string * bool) list
-> Toplevel.transition -> Toplevel.transition
+ val init_context: (string -> unit) -> string -> Toplevel.transition -> Toplevel.transition
val context: string -> Toplevel.transition -> Toplevel.transition
end;
@@ -536,9 +537,10 @@
(* context switch *)
-fun context name =
- Toplevel.init_theory (fn _ => (the (#2 (Context.pass None ThyInfo.quiet_update_thy name))))
- (K ()) (K ());
+fun init_context (f: string -> unit) name =
+ Toplevel.init_theory (fn _ => (the (#2 (Context.pass None f name)))) (K ()) (K ());
+
+val context = init_context (ThyInfo.quiet_update_thy true);
end;