# HG changeset patch
# User wenzelm
# Date 1160600115 -7200
# Node ID 51956522c3068a054a78396234adf2981b815162
# Parent  dbf1eca9b34eded33634106c58463abe3ddb6059
removed 'undo_end', recovered 'cannot_undo';

diff -r dbf1eca9b34e -r 51956522c306 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 11 22:55:14 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 11 22:55:15 2006 +0200
@@ -19,13 +19,13 @@
   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 clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
   val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
   val kill_proof: Toplevel.transition -> Toplevel.transition
   val undo_theory: Toplevel.transition -> Toplevel.transition
-  val undo_end: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
   val kill: Toplevel.transition -> Toplevel.transition
   val back: Toplevel.transition -> Toplevel.transition
@@ -136,6 +136,8 @@
 
 (* history commands *)
 
+fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
+
 val clear_undos_theory = Toplevel.history o History.clear;
 
 val redo =
@@ -158,10 +160,6 @@
 val undo_theory = Toplevel.history (fn hist =>
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
-val undo_end =
-  Toplevel.imperative (fn () => error "Cannot undo end of theory") o
-  undo_theory;
-
 val undo = Toplevel.kill o undo_theory o undos_proof 1;
 val kill = Toplevel.kill o Toplevel.exit_local_theory o kill_proof;