1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Feb 20 14:49:23 2009 +0100
     1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Feb 20 14:49:23 2009 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     Univariate Polynomials
     1.6 -  Id:        $Id$
     1.7    Author:    Clemens Ballarin, started 9 December 1996
     1.8    Copyright: Clemens Ballarin
     1.9  *)
    1.10 @@ -388,7 +387,7 @@
    1.11    proof (cases k)
    1.12      case 0 then show ?thesis by simp ring
    1.13    next
    1.14 -    case Suc then show ?thesis by (simp add: algebra_simps) ring
    1.15 +    case Suc then show ?thesis by simp (ring, simp)
    1.16    qed
    1.17    then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
    1.18  qed