# HG changeset patch
# User wenzelm
# Date 1182810914 -7200
# Node ID 3e3c9d4da4766ef3f26f031ad67f646bacd720aa
# Parent  7e27947d92d797d662e0c467142ef1e67ec6c186
fixed undo: try undos_proof first!

diff -r 7e27947d92d7 -r 3e3c9d4da476 src/Pure/Isar/isar_cmd.ML
--- 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));