--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 19 20:06:21 2016 +0200
@@ -951,7 +951,7 @@
then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
- by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib)
+ by (simp add: norm_mult [symmetric] field_simps setsum_distrib_left)
qed
} note ** = this
show ?thesis