src/Pure/Isar/proof_history.ML
changeset 7366 22a64baa7013
parent 6902 5f126c495771
child 7731 51d59734743d
--- a/src/Pure/Isar/proof_history.ML	Thu Aug 26 11:46:04 1999 +0200
+++ b/src/Pure/Isar/proof_history.ML	Thu Aug 26 19:01:22 1999 +0200
@@ -16,7 +16,7 @@
   val clear: T -> T
   val undo: T -> T
   val redo: T -> T
-  val back: T -> T
+  val back: bool -> T -> T
   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
   val apply: (Proof.state -> Proof.state) -> T -> T
 end;
@@ -55,15 +55,15 @@
 
 (* backtrack *)
 
-fun back_fun ((_, stq), nodes) =
+fun back_fun recur ((_, stq), nodes) =
   (case Seq.pull stq of
     None =>
-      (case nodes of
-        [] => raise FAIL "back: no alternatives"
-      | nd :: nds => (writeln "back: trying previous proof state ..."; back_fun (nd, nds)))
+      if recur andalso not (null nodes) then
+        (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
+      else raise FAIL "back: no alternatives"
   | Some result => (result, nodes));
 
-val back = hist_app back_fun;
+val back = hist_app o back_fun;
 
 
 (* apply transformer *)