back: Toplevel.actual/skip_proof;
use simplified Toplevel.proof etc.;

--- 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