# HG changeset patch
# User wenzelm
# Date 935686882 -7200
# Node ID 22a64baa7013379bac6c581ed7e86618af930203
# Parent  b5bb32e0861c7e8deb0e5e5f2e09684f90516e4f
back: recur flag;

diff -r b5bb32e0861c -r 22a64baa7013 src/Pure/Isar/proof_history.ML
--- 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 *)