diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -1125,7 +1125,7 @@
       using sum.atLeast_Suc_atMost[of 0 "n+1" "\<lambda>i. a$i * b$(n+1-i)"]
       by    (simp add: fps_mult_nth nth_less_subdegree_zero)
     thus "fps_shift 1 (a*b) $ n = (fps_shift 1 a * b) $ n"
-      using sum_shift_bounds_cl_Suc_ivl[of "\<lambda>i. a$i * b$(n+1-i)" 0 n]
+      using sum.shift_bounds_cl_Suc_ivl[of "\<lambda>i. a$i * b$(n+1-i)" 0 n]
       by    (simp add: fps_mult_nth)
   qed
   have "n \<le> subdegree g \<Longrightarrow> fps_shift n (g*h) = fps_shift n g * h"
@@ -2220,7 +2220,7 @@
               "fps_left_inverse (f^2) 1 $ Suc (Suc (Suc k)) =
                 fps_left_inverse (f\<^sup>2) 1 $ Suc (Suc k) * of_nat 2 -
                 fps_left_inverse (f\<^sup>2) 1 $ Suc k"
-              using sum_ub_add_nat f2_nth_simps(1,2) by simp
+              using sum.ub_add_nat f2_nth_simps(1,2) by simp
             also have "\<dots> = of_nat (2 * Suc (Suc (Suc k))) - of_nat (Suc (Suc k))"
               by (subst A, subst B) (simp add: invf2_def mult.commute)
             also have "\<dots> = of_nat (Suc (Suc (Suc k)) + 1)"
@@ -4136,7 +4136,7 @@
     
     from v have "k = sum_list v" by (simp add: A_def natpermute_def)
     also have "\<dots> = (\<Sum>i=0..m. v ! i)"
-      by (simp add: sum_list_sum_nth atLeastLessThanSuc_atLeastAtMost del: sum_op_ivl_Suc)
+      by (simp add: sum_list_sum_nth atLeastLessThanSuc_atLeastAtMost del: sum.op_ivl_Suc)
     also from j have "{0..m} = insert j ({0..m}-{j})" by auto
     also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
       by (subst sum.insert) simp_all
@@ -5927,10 +5927,10 @@
           done
         have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}"
           apply (simp add: pochhammer_minus field_simps m)
-          apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift)
+          apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift simp del: prod.cl_ivl_Suc)
           done
         have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
-          using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift)
+          using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift del: prod.op_ivl_Suc del: prod.cl_ivl_Suc)
           using prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a]
           apply (auto simp add: of_nat_diff field_simps)
           done