diff -r 43d3e087688c -r 955fde69fa7b src/Pure/Isar/isar_thy.ML
--- 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;