src/HOL/Library/Fundamental_Theorem_Algebra.thy

 proof(induct p)
   case 0 thus ?case by simp
 next
   case (pCons c cs)
   {assume c0: "c = 0"
-    from pCons.hyps pCons.prems c0 have ?case apply auto
+    from pCons.hyps pCons.prems c0 have ?case
+      apply (auto)
       apply (rule_tac x="k+1" in exI)
       apply (rule_tac x="a" in exI, clarsimp)
       apply (rule_tac x="q" in exI)
-      by (auto simp add: power_Suc)}
+      by (auto)}
   moreover
   {assume c0: "c\<noteq>0"
     hence ?case apply-
       apply (rule exI[where x=0])
       apply (rule exI[where x=c], clarsimp)