src/HOL/Old_Number_Theory/Finite2.thy

--- a/src/HOL/Old_Number_Theory/Finite2.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -55,7 +55,7 @@
 subsection {* Cardinality of explicit finite sets *}
 
 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
-  by (simp add: finite_subset finite_imageI)
+by (simp add: finite_subset)
 
 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
   by (rule bounded_nat_set_is_finite) blast