--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Nov 22 10:06:31 2018 +0000
@@ -3378,8 +3378,8 @@
(is "?l = ?r")
proof -
let ?KM = "{(k,m). k + m \<le> n}"
- let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
- have th0: "?KM = UNION {0..n} ?f"
+ let ?f = "\<lambda>s. \<Union>i\<in>{0..s}. {(i, s - i)}"
+ have th0: "?KM = \<Union> (?f ` {0..n})"
by auto
show "?l = ?r "
unfolding th0