removed obsolete init_context;
authorwenzelm
Fri, 29 Dec 2006 19:50:48 +0100
changeset 21947 ccce5aea39b1
parent 21946 78e018d1f845
child 21948 e34bc5e4e7bc
removed obsolete init_context;
src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 18:47:11 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 19:50:48 2006 +0100
@@ -31,7 +31,6 @@
   val kill_theory: string -> unit
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
-  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
   val welcome: Toplevel.transition -> Toplevel.transition
   val init_toplevel: Toplevel.transition -> Toplevel.transition
   val exit: Toplevel.transition -> Toplevel.transition
@@ -204,13 +203,6 @@
     (fn thy => (end_theory thy; ()))
     (kill_theory o Context.theory_name);
 
-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 ());
-
 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
 
 val welcome = Toplevel.imperative (writeln o Session.welcome);