1.1 --- a/src/ZF/CardinalArith.ML	Fri Mar 31 02:00:29 1995 +0200
     1.2 +++ b/src/ZF/CardinalArith.ML	Fri Mar 31 10:58:14 1995 +0200
     1.3 @@ -412,10 +412,8 @@
     1.4  goalw CardinalArith.thy [inj_def]
     1.5   "!!K. Ord(K) ==>	\
     1.6  \ (lam z:K*K. split(%x y. <x Un y, <x, y>>, z)) : inj(K*K, K*K*K)";
     1.7 -by (safe_tac ZF_cs);
     1.8 -by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI]
     1.9 -                    addSEs [split_type]) 1);
    1.10 -by (asm_full_simp_tac ZF_ss 1);
    1.11 +by (fast_tac (ZF_cs addss ZF_ss
    1.12 +		    addIs [lam_type, Un_least_lt RS ltD, ltI]) 1);
    1.13  qed "csquare_lam_inj";
    1.14  
    1.15  goalw CardinalArith.thy [csquare_rel_def]