diff -r c64628dbac00 -r ff12606337e9 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -464,7 +464,7 @@
   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   show "convex (closed_segment 0 z)"
-    by (rule convex_segment [of 0 z])
+    by (rule convex_closed_segment [of 0 z])
 next
   fix k x
   assume "x \<in> closed_segment 0 z" "k \<le> n"