--- a/src/Pure/Isar/isar.ML Tue Jul 15 11:02:43 2008 +0200
+++ b/src/Pure/Isar/isar.ML Tue Jul 15 11:50:02 2008 +0200
@@ -15,7 +15,6 @@
val print: unit -> unit
val >> : Toplevel.transition -> bool
val >>> : Toplevel.transition list -> unit
- val commit_exit: unit -> unit
val linear_undo: int -> unit
val undo: int -> unit
val kill: unit -> unit
@@ -167,19 +166,6 @@
fun print () = Toplevel.print_state false (state ());
-(* commit final exit *)
-
-fun commit_exit () =
- let val (id, (st, _)) = point_result () in
- (case (Toplevel.is_toplevel st, prev_command id) of
- (true, SOME prev) =>
- (case Toplevel.transition true Toplevel.commit_exit (#1 (the_result prev)) of
- SOME (_, SOME err) => error (Toplevel.exn_message (Toplevel.EXCURSION_FAIL err))
- | _ => init_point ())
- | _ => error "Expected to find finished theory")
- end;
-
-
(* interactive state transformations --- NOT THREAD-SAFE! *)
nonfix >> >>>;