src/HOL/equalities.ML

 Goal "insert a A = {a} Un A";
 by (Blast_tac 1);
 qed "insert_is_Un";
 
 Goal "insert a A ~= {}";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"insert_not_empty";
 Addsimps[insert_not_empty];
 
 bind_thm("empty_not_insert",insert_not_empty RS not_sym);
 Addsimps[empty_not_insert];

 by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
 
 Goal "(f`A = {}) = (A = {})";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
 (*NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   with its implicit quantifier and conjunction.  Also image enjoys better

 by (Blast_tac 1);
 qed "Int_empty_right";
 Addsimps[Int_empty_right];
 
 Goal "(A Int B = {}) = (A <= -B)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "disjoint_eq_subset_Compl";
 
 Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
 by  (Blast_tac 1);
 qed "disjoint_iff_not_equal";

 Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
 by (Blast_tac 1);
 qed "Int_Un_distrib2";
 
 Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
 Goal "(C <= A Int B) = (C <= A & C <= B)";
 by (Blast_tac 1);

 \     (A Un B) Int (B Un C) Int (C Un A)";
 by (Blast_tac 1);
 qed "Un_Int_crazy";
 
 Goal "(A<=B) = (A Un B = B)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "subset_Un_eq";
 
 Goal "(A Un B = {}) = (A = {} & B = {})";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Un_empty";
 AddIffs[Un_empty];
 
 Goal "(A Un B <= C) = (A <= C & B <= C)";
 by (Blast_tac 1);

 by (Blast_tac 1);
 qed "subset_Compl_self_eq";
 
 (*Halmos, Naive Set Theory, page 16.*)
 Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Un_Int_assoc_eq";
 
 Goal "-UNIV = {}";
 by (Blast_tac 1);
 qed "Compl_UNIV_eq";

 by Auto_tac; 
 qed "Union_empty_conv"; 
 AddIffs [Union_empty_conv];
 
 Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Union_disjoint";
 
 section "Inter";
 
 Goal "Inter({}) = UNIV";