src/HOL/Nonstandard_Analysis/HSeries.thy

--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -81,7 +81,7 @@
 lemma sumhr_shift_bounds:
   "\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
     sumhr (m, n, \<lambda>i. f (i + k))"
-  unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
+  unfolding sumhr_app by transfer (rule sum.shift_bounds_nat_ivl)
 
 
 subsection \<open>Nonstandard Sums\<close>