diff -r 3928b3448f38 -r f4a7697011c5 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 26 22:53:06 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 27 19:34:30 2011 +0200
@@ -280,14 +280,18 @@
        blast
 qed
 
-lemma finite_vimageI:
-  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
+lemma finite_vimage_IntI:
+  "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
   apply (induct rule: finite_induct)
    apply simp_all
   apply (subst vimage_insert)
-  apply (simp add: finite_subset [OF inj_vimage_singleton])
+  apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
   done
 
+lemma finite_vimageI:
+  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
+  using finite_vimage_IntI[of F h UNIV] by auto
+
 lemma finite_vimageD:
   assumes fin: "finite (h -` F)" and surj: "surj h"
   shows "finite F"