src/Pure/Isar/proof_history.ML

   val current: T -> Proof.state
   val previous: T -> Proof.state option
   val clear: int -> T -> T
   val undo: T -> T
   val redo: T -> T
-  val back: bool -> T -> T
+  val back: T -> T
   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
   val apply: (Proof.state -> Proof.state) -> T -> T
 end;
 
 structure ProofHistory: PROOF_HISTORY =

 val clear = app o History.clear;
 val undo = app History.undo;
 val redo = app History.redo;
 
 
-(* backtrack *)
+(* backtracking *)
 
-fun backtrack recur ((_, stq), nodes) =
+val back = hist_app (fn ((_, stq), nodes) =>
   (case Seq.pull stq of
-    NONE =>
-      if recur andalso not (null nodes) then
-        (writeln "back: trying previous proof state ..."; backtrack recur (hd nodes, tl nodes))
-      else raise FAIL "back: no alternatives"
-  | SOME result => (result, nodes));
-
-val back = hist_app o backtrack;
+    NONE => raise FAIL "back: no alternatives"
+  | SOME result => (result, nodes)));
 
 
 (* apply transformer *)
 
 fun applys f = hist_app (fn (node as (st, _), nodes) =>