removed obsolete init_context;
authorwenzelm
Fri Dec 29 19:50:48 2006 +0100 (2006-12-29)
changeset 21947ccce5aea39b1
parent 21946 78e018d1f845
child 21948 e34bc5e4e7bc
removed obsolete init_context;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 18:47:11 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 19:50:48 2006 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    val kill_theory: string -> unit
     1.5    val theory: string * string list * (string * bool) list
     1.6      -> Toplevel.transition -> Toplevel.transition
     1.7 -  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
     1.8    val welcome: Toplevel.transition -> Toplevel.transition
     1.9    val init_toplevel: Toplevel.transition -> Toplevel.transition
    1.10    val exit: Toplevel.transition -> Toplevel.transition
    1.11 @@ -204,13 +203,6 @@
    1.12      (fn thy => (end_theory thy; ()))
    1.13      (kill_theory o Context.theory_name);
    1.14  
    1.15 -fun init_context f x = Toplevel.init_theory
    1.16 -  (fn _ =>
    1.17 -    (case Context.pass NONE f x of
    1.18 -      ((), NONE) => raise Toplevel.UNDEF
    1.19 -    | ((), SOME thy) => thy))
    1.20 -  (K ()) (K ());
    1.21 -
    1.22  val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    1.23  
    1.24  val welcome = Toplevel.imperative (writeln o Session.welcome);