diff -r 1b43d9184bf5 -r ac78eee049ce src/Pure/Isar/isar_cmd.ML
--- 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 =