diff -r 179ff9cb160b -r 5b25fee0362c src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -1,6 +1,5 @@
 (*
   Title:     Univariate Polynomials
-  Id:        $Id$
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 *)
@@ -388,7 +387,7 @@
   proof (cases k)
     case 0 then show ?thesis by simp ring
   next
-    case Suc then show ?thesis by (simp add: algebra_simps) ring
+    case Suc then show ?thesis by simp (ring, simp)
   qed
   then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
 qed