src/HOL/Finite.ML

 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
 val lemma = result();
 
 
 Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
-by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
+by (blast_tac (claset() addIs [rulify lemma]) 1);
 qed "foldSet_determ";
 
 Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
 by (blast_tac (claset() addIs [foldSet_determ]) 1);
 qed "fold_equality";