diff -r d995733b635d -r f0de18b62d63 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Convex.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -129,7 +129,7 @@
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     from this asms
     have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
     hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
@@ -410,7 +410,7 @@
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     have "convex C" using asms by auto
     hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
       using asms convex_setsum[OF `finite s`
@@ -433,7 +433,7 @@
       using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
         OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
     also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
-      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
+      unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
     also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
     also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
     finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"