--- 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);