# HG changeset patch
# User wenzelm
# Date 1124192564 -7200
# Node ID dc1040419645c872c8b3b109abe4f707aaab5a4b
# Parent  501c28052aea0834f776baab5533e1619e3528af
back: removed ill-defined '!' option;

diff -r 501c28052aea -r dc1040419645 src/Pure/Isar/proof_history.ML
--- a/src/Pure/Isar/proof_history.ML	Tue Aug 16 13:42:43 2005 +0200
+++ b/src/Pure/Isar/proof_history.ML	Tue Aug 16 13:42:44 2005 +0200
@@ -17,7 +17,7 @@
   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;
@@ -55,17 +55,12 @@
 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 *)