stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
even for conditional rewrites

--- a/src/FOL/IFOL.ML	Mon Jul 13 17:46:20 1998 +0200
+++ b/src/FOL/IFOL.ML	Tue Jul 14 13:29:39 1998 +0200
@@ -238,7 +238,9 @@
 
 (*Substitution: rule and tactic*)
 bind_thm ("ssubst", sym RS subst);
-fun stac th = CHANGED o rtac (th RS ssubst);
+
+(*Fails unless the substitution has an effect*)
+fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
 
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 qed_goal "ex1_equalsE" IFOL.thy

--- a/src/HOL/HOL.ML	Mon Jul 13 17:46:20 1998 +0200
+++ b/src/HOL/HOL.ML	Tue Jul 14 13:29:39 1998 +0200
@@ -343,7 +343,9 @@
 
 (** Standard abbreviations **)
 
-fun stac th = CHANGED o rtac (th RS ssubst);
+(*Fails unless the substitution has an effect*)
+fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
+
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);