--- a/src/HOL/ex/ThreeDivides.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -199,7 +199,7 @@
       by (simp add: div_mult2_eq[symmetric])
     also have
       "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
-      by (simp only: sum_shift_bounds_Suc_ivl)
+      by (simp only: sum.shift_bounds_Suc_ivl)
          (simp add: atLeast0LessThan)
     also have
       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"