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