--- a/src/HOL/Finite_Set.thy Fri Sep 18 14:09:38 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sat Sep 19 07:38:03 2009 +0200
@@ -1566,8 +1566,6 @@
prefer 2
apply assumption
apply auto
- apply (rule setsum_cong)
- apply auto
done
lemma setsum_right_distrib: