diff -r a99a0f5474c5 -r 6ec272e153f0 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Feb 13 07:48:42 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Wed Feb 13 09:50:16 2019 +0100
@@ -1203,7 +1203,7 @@
         have c: "card (S - {x}) = card S - 1"
           by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
         have "sum u (S - {x}) = 1 - u x"
-          by (simp add: Suc.prems sum_diff1_ring \<open>x \<in> S\<close>)
+          by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>)
         with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
           by auto
         have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"