# HG changeset patch
# User wenzelm
# Date 1167418248 -3600
# Node ID ccce5aea39b194e93b986e6f1b91df60271c4d2e
# Parent  78e018d1f8454bb890648599092eaa9750b3f732
removed obsolete init_context;

diff -r 78e018d1f845 -r ccce5aea39b1 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);