src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/Finite.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -570,7 +570,7 @@
 
 
 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";