--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 13 16:02:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 13 17:48:33 2015 +0100
@@ -9470,7 +9470,7 @@
have "?x = norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
unfolding split_def setsum_subtractf ..
also have "\<dots> \<le> e + k"
- apply (rule *[OF **, where ir2="setsum (\<lambda>k. integral k f) r"])
+ apply (rule *[OF **, where ir1="setsum (\<lambda>k. integral k f) r"])
proof goal_cases
case 1
have *: "k * real (card r) / (1 + real (card r)) < k"