src/Pure/tctical.ML

--- a/src/Pure/tctical.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/tctical.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -6,7 +6,7 @@
 Tacticals
 *)
 
-infix 1 THEN THEN' THEN_MAYBE THEN_MAYBE';
+infix 1 THEN THEN';
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
 infix 0 THEN_ELSE;
 
@@ -55,8 +55,6 @@
   val suppress_tracing  : bool ref
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val THEN_MAYBE	: tactic * tactic -> tactic
-  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
   val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
   val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
@@ -148,21 +146,34 @@
 (*Do the tactic or else do nothing*)
 fun TRY tac = tac ORELSE all_tac;
 
-(*Execute tac1, but only execute tac2 if there are at least as many subgoals
-  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
-fun tac1 THEN_MAYBE tac2 = let fun has_fewer_prems n rule = (nprems_of rule < n)
-in STATE (fn state => tac1  THEN  
-	 COND (has_fewer_prems (nprems_of state)) all_tac tac2) end;
-fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
+(*** List-oriented tactics ***)
+
+local
+  (*This version of EVERY avoids backtracking over repeated states*)
+
+  fun EVY (trail, []) st = 
+	Sequence.seqof (fn()=> Some(st, 
+			Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
+    | EVY (trail, tac::tacs) st = 
+	  case Sequence.pull(tac st) of
+	      None    => evyBack trail              (*failed: backtrack*)
+	    | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
+  and evyBack [] = Sequence.null (*no alternatives*)
+    | evyBack ((st',q,tacs)::trail) =
+	  case Sequence.pull q of
+	      None        => evyBack trail
+	    | Some(st,q') => if eq_thm (st',st) 
+			     then evyBack ((st',q',tacs)::trail)
+			     else EVY ((st,q',tacs)::trail, tacs) st
+in
+
+(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
+fun EVERY tacs = EVY ([], tacs);
+end;
 
 
-(*** List-oriented tactics ***)
-
-(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
-fun EVERY tacs = foldr (op THEN) (tacs, all_tac);
-
 (* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
-fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac);
+fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
 
 (*Apply every tactic to 1*)
 fun EVERY1 tacs = EVERY' tacs 1;