src/HOL/Library/Formal_Power_Series.thy

--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -3181,7 +3181,7 @@
   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"
-    by (auto simp add: set_eq_iff Bex_def)
+    by auto
   show "?l = ?r "
     unfolding th0
     apply (subst setsum.UNION_disjoint)