# HG changeset patch
# User paulson
# Date 900415779 -7200
# Node ID 013ea0f023e30db39e108ae068c705db179943bb
# Parent  b02dfb930bd9b823a721d1b71952a1c14883219e
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
even for conditional rewrites

diff -r b02dfb930bd9 -r 013ea0f023e3 src/FOL/IFOL.ML
--- 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
diff -r b02dfb930bd9 -r 013ea0f023e3 src/HOL/HOL.ML
--- 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);