src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -334,7 +334,7 @@
     using finite_subset_image [OF B] P by blast
 qed blast
 
-lemma exists_finite_subset_image:
+lemma ex_finite_subset_image:
   "(\<exists>B. finite B \<and> B \<subseteq> f ` A \<and> P B) \<longleftrightarrow> (\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B))"
 proof safe
   fix B :: "'a set"