src/HOL/Finite_Set.thy

   apply (erule finite_subset, assumption)
   done
 
 lemma finite_range_imageI:
     "finite (range g) ==> finite (range (%x. f (g x)))"
-  apply (drule finite_imageI, simp)
+  apply (drule finite_imageI, simp add: range_composition)
   done
 
 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
 proof -
   have aux: "!!A. finite (A - {}) = finite A" by simp