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