--- 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"