# HG changeset patch
# User paulson
# Date 843750171 -7200
# Node ID 2c2a95cbb5c95387ca2da72d96e3961966a27c0b
# Parent  62ff902eeffc7a2d79176f7808459c1badd8fd4d
Declared stac

diff -r 62ff902eeffc -r 2c2a95cbb5c9 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Thu Sep 26 16:38:02 1996 +0200
+++ b/src/FOL/IFOL.ML	Thu Sep 26 17:02:51 1996 +0200
@@ -225,8 +225,9 @@
 (** ~ b=a ==> ~ a=b **)
 val [not_sym] = compose(sym,2,contrapos);
 
-(*calling "standard" reduces maxidx to 0*)
-bind_thm ("ssubst", (sym RS subst));
+(*Substitution: rule and tactic*)
+bind_thm ("ssubst", sym RS subst);
+fun stac th = CHANGED o rtac (th RS ssubst);
 
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 qed_goal "ex1_equalsE" IFOL.thy