diff -r c4f2cac288d2 -r 4005298550a6 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Wed Apr 10 13:34:55 2019 +0100
@@ -272,8 +272,8 @@
     with *[rule_format, of "2" ?u ?x] have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s"
       using mu xy by auto
     have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
-      using sum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
-    from sum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
+      using sum.atLeast_Suc_atMost[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
+    from sum.atLeast_Suc_atMost[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
     have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
       by auto
     then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"