src/Pure/Isar/isar_thy.ML

   val begin_theory: string -> string list -> (string * bool) list -> theory
   val end_theory: theory -> theory
   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;
 
 structure IsarThy: ISAR_THY =
 struct

 fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name);
 
 
 (* 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;