--- a/src/HOL/Library/Indicator_Function.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Sun Nov 18 18:07:51 2018 +0000
@@ -191,7 +191,7 @@
\<close>
lemma indicator_UN_disjoint:
- "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
+ "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
by (induct A rule: finite_induct)
(auto simp: disjoint_family_on_def indicator_def split: if_splits)