diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -138,7 +138,7 @@
     with `0 \<le> setsum a s` have "0 < setsum a s" by simp
     then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
       using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
-      by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
+      by (simp add: IH setsum_divide_distrib [symmetric])
     from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
       and `0 \<le> setsum a s` and `a i + setsum a s = 1`
     have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
@@ -432,9 +432,7 @@
     then have "a i < 1" using asm by auto
     then have i0: "1 - a i > 0" by auto
     let ?a = "\<lambda>j. a j / (1 - a i)"
-    { fix j assume "j \<in> s"
-      then have "?a j \<ge> 0"
-        using i0 asms divide_nonneg_pos
+    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
         by fastforce }
     note a_nonneg = this
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto