removed obsolete clear_undos_theory;
undo/cannot_undo: proper undo of 'end';

--- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 20:35:03 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 30 12:33:25 2006 +0100
@@ -43,14 +43,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: Toplevel.transition -> Toplevel.transition
+  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val kill: Toplevel.transition -> Toplevel.transition
   val back: Toplevel.transition -> Toplevel.transition
   val use: Path.T -> Toplevel.transition -> Toplevel.transition
@@ -240,10 +239,6 @@
 
 (* 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 =
   Toplevel.history History.redo o
   Toplevel.actual_proof ProofHistory.redo o
@@ -264,7 +259,11 @@
 val undo_theory = Toplevel.history (fn hist =>
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
-val undo = Toplevel.kill o undo_theory o undos_proof 1;
+val undo = Toplevel.kill o undos_proof 1 o undo_theory o Toplevel.undo_exit;
+
+fun cannot_undo "end" = undo   (*ProofGeneral legacy*)
+  | cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
+
 val kill = Toplevel.kill o kill_proof;
 
 val back =