diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy	Wed Apr 10 21:29:32 2019 +0100
@@ -23,7 +23,7 @@
   also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
     by (simp add: sum_distrib_left ac_simps)
   also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
-    by (simp add: nested_sum_swap')
+    by (simp add: sum.nested_swap')
   finally show ?thesis .
 qed