diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Transcendental.thy	Mon Jan 14 14:46:12 2019 +0100
@@ -6088,7 +6088,7 @@
   also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
     by (simp add: sum.Sigma)
   also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
-    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
     by (simp add: sum.Sigma)
   also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
@@ -6110,7 +6110,7 @@
       apply (rule_tac x="x + Suc j" in image_eqI, auto)
       done
     then show ?thesis
-      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   qed
   then show ?thesis
     by (simp add: polyfun_diff [OF assms] sum_distrib_right)