--- a/src/HOL/Big_Operators.thy Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Big_Operators.thy Sun Nov 28 15:20:51 2010 +0100
@@ -707,7 +707,7 @@
proof -
have "A <+> B = Inl ` A \<union> Inr ` B" by auto
moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
- by(auto intro: finite_imageI)
+ by auto
moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)