# HG changeset patch # User wenzelm # Date 1129651172 -7200 # Node ID 0e0ac7700f57274826aeebc3253f6455fc9a7eac # Parent ff78ecd1e768eeede61851bf46ac52e7fcb3b612 back: Toplevel.actual/skip_proof; use simplified Toplevel.proof etc.; diff -r ff78ecd1e768 -r 0e0ac7700f57 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Oct 18 17:59:31 2005 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 18 17:59:32 2005 +0200 @@ -160,7 +160,10 @@ val undo = Toplevel.kill o undo_theory o undos_proof 1; val kill = Toplevel.kill o kill_proof; -val back = Toplevel.proof ProofHistory.back; + +val back = + Toplevel.actual_proof ProofHistory.back o + Toplevel.skip_proof (History.apply I); (* use ML text *) @@ -372,8 +375,7 @@ raise Toplevel.UNDEF)); fun theory f (loc, txt) = enter_locale loc o present_text false f loc txt; -fun proof f txt = - Toplevel.print o Toplevel.proof (ProofHistory.apply I) o present_text true f NONE txt; +fun proof f txt = Toplevel.print o Toplevel.proof I o present_text true f NONE txt; in