src/HOL/HOL.ML
changeset 5139 013ea0f023e3
parent 4527 4878fb3d0ac5
child 5154 40fd46f3d3a1
--- 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);