src/HOL/Integ/Equiv.ML
changeset 2036 62ff902eeffc
parent 1978 e7df069acb74
child 2215 ebf910e7ec87
     1.1 --- a/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:12:25 1996 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:38:02 1996 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4  \    ==> (UN x:X. b(x)) : B";
     1.5  by (cut_facts_tac prems 1);
     1.6  by (safe_tac (!claset));
     1.7 -by (rtac (localize UN_equiv_class RS ssubst) 1);
     1.8 +by (stac (localize UN_equiv_class) 1);
     1.9  by (REPEAT (ares_tac prems 1));
    1.10  qed "UN_equiv_class_type";
    1.11