Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed undo: try undos_proof first!
authorwenzelm
Tue, 26 Jun 2007 00:35:14 +0200
changeset 23500 3e3c9d4da476
parent 23499 7e27947d92d7
child 23501 e5874335a655
fixed undo: try undos_proof first!
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 25 22:46:55 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 26 00:35:14 2007 +0200
@@ -369,7 +369,7 @@
 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 undos_proof 1 o undo_theory o Toplevel.undo_exit;
+val undo = Toplevel.kill o undo_theory o Toplevel.undo_exit o undos_proof 1;
 
 fun cannot_undo "end" = undo   (*ProofGeneral legacy*)
   | cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
isabelle