diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Wed Jan 02 15:14:02 2008 +0100
@@ -181,6 +181,6 @@
   "EVAL (y::'a::domain)
     (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
    x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
-  by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
+  by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
 
 end