src/HOL/Library/Convex.thy

--- a/src/HOL/Library/Convex.thy	Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Library/Convex.thy	Sat Jun 13 13:09:05 2015 +0200
@@ -538,7 +538,7 @@
       by auto
     let ?a = "\<lambda>j. a j / (1 - a i)"
     have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
-      using i0 insert prems by fastforce
+      using i0 insert that by fastforce
     have "(\<Sum> j \<in> insert i s. a j) = 1"
       using insert by auto
     then have "(\<Sum> j \<in> s. a j) = 1 - a i"