tuned;

--- a/src/Pure/Isar/toplevel.ML	Sat Jul 24 21:22:21 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 24 21:40:48 2010 +0200
@@ -295,7 +295,7 @@
 datatype trans =
   Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
   Exit |                                         (*formal exit of theory -- without committing*)
-  CommitExit |                                   (*exit and commit final theory*)
+  Commit_Exit |                                  (*exit and commit final theory*)
   Keep of bool -> state -> unit |                (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
@@ -306,7 +306,7 @@
           (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
-  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
+  | apply_tr _ Commit_Exit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
       (Runtime.controlled_execution exit thy; toplevel)
   | apply_tr int (Keep f) state =
       Runtime.controlled_execution (fn x => tap (f int) x) state
@@ -648,7 +648,7 @@
 fun commit_exit pos =
   name "end" empty
   |> position pos
-  |> add_trans CommitExit
+  |> add_trans Commit_Exit
   |> imperative (fn () => warning "Expected to find finished theory");