removed obsolete context;
authorwenzelm
Sat, 11 Nov 2006 16:11:44 +0100
changeset 21307 c432585af03b
parent 21306 7ab6e95e6b0b
child 21308 73883a528b26
removed obsolete context;
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;