diff -r 4898bae6ef23 -r 0a54cfc9add3 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -94,7 +94,7 @@
 subsection {* Properties of SetS *}
 
 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
-  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
+  by (auto simp add: SetS_def SRStar_finite [of p])
 
 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
   by (auto simp add: SetS_def MultInvPair_def)