diff -r f9bf65d90b69 -r 0f31dd2e540d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 19:48:41 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 21:00:50 2018 +0100
@@ -5924,7 +5924,7 @@
       next
         have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
               \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
-          apply (subst sum_group)
+          apply (subst sum.group)
           using s by (auto simp: sum_subtractf split_def p'(1))
         also have "\<dots> < e/2"
         proof -