diff -r 304a47739407 -r 04ce6bb14d85 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu Sep 24 19:14:18 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Fri Sep 25 09:50:31 2009 +0200
@@ -3649,10 +3649,7 @@
     from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
       unfolding cond_value_iff cond_application_beta
-      apply (simp add: cond_value_iff cong del: if_weak_cong)
-      apply (rule setsum_cong)
-      apply auto
-      done
+      by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong)
     hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
     hence "y \<in> ?rhs" by auto}
   moreover