1.1 --- a/src/HOL/Finite.ML	Tue Sep 05 10:12:20 2000 +0200
     1.2 +++ b/src/HOL/Finite.ML	Tue Sep 05 10:12:48 2000 +0200
     1.3 @@ -543,14 +543,14 @@
     1.4  by (rename_tac "Aa xa ya Ab xb yb" 1);
     1.5   by (case_tac "xa=xb" 1);
     1.6   by (subgoal_tac "Aa = Ab" 1);
     1.7 - by (blast_tac (claset() addEs [equalityE]) 2);
     1.8 + by (blast_tac (claset() addSEs [equalityE]) 2);
     1.9   by (Blast_tac 1);
    1.10  (*case xa ~= xb*)
    1.11  by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
    1.12 - by (blast_tac (claset() addEs [equalityE]) 2);
    1.13 + by (blast_tac (claset() addSEs [equalityE]) 2);
    1.14  by (Clarify_tac 1);
    1.15  by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
    1.16 - by (blast_tac (claset() addEs [equalityE]) 2);
    1.17 + by (Blast_tac 2);
    1.18  (** LEVEL 20 **)
    1.19  by (subgoal_tac "card Aa <= card Ab" 1);
    1.20   by (rtac (Suc_le_mono RS subst) 2);
    1.21 @@ -560,11 +560,12 @@
    1.22  by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
    1.23  by (ftac Diff1_foldSet 1 THEN assume_tac 1);
    1.24  by (subgoal_tac "ya = f xb x" 1);
    1.25 - by (Blast_tac 2);
    1.26 + by (blast_tac (claset() delrules [equalityCE]) 2);
    1.27  by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
    1.28   by (Asm_full_simp_tac 2);
    1.29  by (subgoal_tac "yb = f xa x" 1);
    1.30 - by (blast_tac (claset() addDs [Diff1_foldSet]) 2);
    1.31 + by (blast_tac (claset() delrules [equalityCE]
    1.32 +			addDs [Diff1_foldSet]) 2);
    1.33  by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
    1.34  val lemma = result();
    1.35