# HG changeset patch
# User wenzelm
# Date 1163257904 -3600
# Node ID c432585af03b592e2d880ea52b47dad824f3eb33
# Parent  7ab6e95e6b0b4bba32e0c5f3186edc74362cb132
removed obsolete context;

diff -r 7ab6e95e6b0b -r c432585af03b src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sat Nov 11 16:11:43 2006 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Sat Nov 11 16:11:44 2006 +0100
@@ -34,7 +34,6 @@
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
   val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
-  val context: string -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure IsarThy: ISAR_THY =
@@ -132,16 +131,11 @@
     (fn thy => (end_theory thy; ()))
     (kill_theory o Context.theory_name);
 
-
-(* context switch *)
-
-fun fetch_context f x =
-  (case Context.pass NONE f x of
-    ((), NONE) => raise Toplevel.UNDEF
-  | ((), SOME thy) => thy);
-
-fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());
-
-val context = init_context (ThyInfo.quiet_update_thy true);
+fun init_context f x = Toplevel.init_theory
+  (fn _ =>
+    (case Context.pass NONE f x of
+      ((), NONE) => raise Toplevel.UNDEF
+    | ((), SOME thy) => thy))
+  (K ()) (K ());
 
 end;