diff -r 9624711ef2de -r a6f5a78712af src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jan 26 21:16:03 2018 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Jan 27 10:27:57 2018 +0100
@@ -485,6 +485,12 @@
 lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A"
   by (blast intro: finite_subset [OF subset_Pow_Union])
 
+lemma finite_bind:
+  assumes "finite S"
+  assumes "\<forall>x \<in> S. finite (f x)"
+  shows "finite (Set.bind S f)"
+using assms by (simp add: bind_UNION)
+
 lemma finite_set_of_finite_funs:
   assumes "finite A" "finite B"
   shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")