--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 19 20:06:21 2016 +0200
@@ -235,7 +235,7 @@
by auto
also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
(epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
- by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
+ by (subst setsum.distrib) (simp add: field_simps setsum_distrib_left)
also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
apply (rule add_left_mono)
apply (rule mult_left_mono)