# HG changeset patch
# User wenzelm
# Date 1185132056 -7200
# Node ID 2807ecdc853d0f0475d77dab295d40dbae367444
# Parent  30e1eb0c5b2f25bbc23d77179b1a952634946878
init_empty: invoke operation *after* safe_exit;

diff -r 30e1eb0c5b2f -r 2807ecdc853d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jul 22 21:20:55 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -56,7 +56,7 @@
   val no_timing: transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
     transition -> transition
-  val init_empty: (state -> unit) -> transition -> transition
+  val init_empty: (unit -> unit) -> transition -> transition
   val exit: transition -> transition
   val undo_exit: transition -> transition
   val kill: transition -> transition
@@ -387,7 +387,7 @@
 datatype trans =
   Init of (bool -> theory) * ((theory -> unit) * (theory -> unit)) |
                                                     (*init node; with exit/kill operation*)
-  InitEmpty of state -> unit |                      (*init empty toplevel*)
+  InitEmpty of unit -> unit |                       (*init empty toplevel*)
   Exit |                                            (*conclude node -- deferred until init*)
   UndoExit |                                        (*continue after conclusion*)
   Kill |                                            (*abort node*)
@@ -410,8 +410,8 @@
 fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
       let val node = Theory (Context.Theory (f int), NONE)
       in safe_exit state; State (History.init (undo_limit int) node, term) end
-  | apply_tr int _ (InitEmpty f) state =
-      (keep_state int (K f) state; safe_exit state; toplevel)
+  | apply_tr int _ (InitEmpty f) (state as Toplevel _) =
+      (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
   | apply_tr _ _ Exit (State (node, term)) =
       (the_global_theory (History.current node); Toplevel (SOME (node, term)))
   | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info