diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -13,7 +13,7 @@
 
 lemma sum_mult_product:
   "sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
-  unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
+  unfolding sum.nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
 proof (rule sum.cong, simp, rule sum.reindex_cong)
   fix i
   show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)