src/HOL/Analysis/Poly_Roots.thy

--- a/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy	Wed Apr 10 13:34:55 2019 +0100
@@ -174,7 +174,7 @@
    have "\<exists>k\<le>n. b k \<noteq> 0"
      apply (rule ccontr)
      using polyfun_extremal [OF extr_prem, of 1]
-     apply (auto simp: eventually_at_infinity b simp del: sum_atMost_Suc)
+     apply (auto simp: eventually_at_infinity b simp del: sum.atMost_Suc)
      apply (drule_tac x="of_real ba" in spec, simp)
      done
    then show ?thesis using Suc.IH [of b] ins_ab