1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 25 22:46:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 26 00:35:14 2007 +0200
     1.3 @@ -369,7 +369,7 @@
     1.4  val undo_theory = Toplevel.history (fn hist =>
     1.5    if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
     1.6  
     1.7 -val undo = Toplevel.kill o undos_proof 1 o undo_theory o Toplevel.undo_exit;
     1.8 +val undo = Toplevel.kill o undo_theory o Toplevel.undo_exit o undos_proof 1;
     1.9  
    1.10  fun cannot_undo "end" = undo   (*ProofGeneral legacy*)
    1.11    | cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));