1.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 24 19:14:18 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Sep 25 09:50:31 2009 +0200
     1.3 @@ -1565,9 +1565,7 @@
     1.4    apply (rule finite_subset)
     1.5    prefer 2
     1.6    apply assumption
     1.7 -  apply auto
     1.8 -  apply (rule setsum_cong)
     1.9 -  apply auto
    1.10 +  apply (auto simp add: sup_absorb2)
    1.11  done
    1.12  
    1.13  lemma setsum_right_distrib: