# HG changeset patch
# User oheimb
# Date 856019107 -3600
# Node ID 4ee01bb55a444c6e272aa90db05421234842e039
# Parent  373daa468a740e4644509ae45ceae5b384c9c8aa
added THEN_MAYBE and THEN_MAYBE'

diff -r 373daa468a74 -r 4ee01bb55a44 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Sat Feb 15 16:04:33 1997 +0100
+++ b/src/Pure/tctical.ML	Sat Feb 15 16:05:07 1997 +0100
@@ -6,9 +6,8 @@
 Tacticals
 *)
 
-infix 1 THEN THEN';
+infix 1 THEN THEN' THEN_MAYBE THEN_MAYBE';
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
-
 infix 0 THEN_ELSE;
 
 
@@ -56,6 +55,8 @@
   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
@@ -147,6 +148,13 @@
 (*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 ***)