added undo_end;

--- a/src/Pure/Isar/isar_cmd.ML	Sat Sep 30 21:39:27 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Sep 30 21:39:29 2006 +0200
@@ -19,7 +19,7 @@
   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
-  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
+  val undo_end: string -> Toplevel.transition -> Toplevel.transition
   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
@@ -136,7 +136,7 @@
 
 (* history commands *)
 
-fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
+fun undo_end txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
 val clear_undos_theory = Toplevel.history o History.clear;
 
 val redo =

--- a/src/Pure/Isar/isar_syn.ML	Sat Sep 30 21:39:27 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 30 21:39:29 2006 +0200
@@ -618,9 +618,13 @@
 
 (* history *)
 
-val cannot_undoP =
-  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
-    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
+val cannot_undoP =    (* FIXME ProofGeneral compatibility *)
+  OuterSyntax.improper_command "cannot_undo" "attempt to undo 'end'" K.control
+    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
+
+val undo_endP =
+  OuterSyntax.improper_command "undo_end" "attempt to undo 'end'" K.control
+    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
 
 val clear_undosP =
   OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
@@ -910,8 +914,8 @@
   terminal_proofP, default_proofP, immediate_proofP, done_proofP,
   skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
   proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
-  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
-  interpretationP, interpretP,
+  cannot_undoP, undo_endP, clear_undosP, redoP, undos_proofP, undoP,
+  killP, interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,