# HG changeset patch
# User haftmann
# Date 1235137763 -3600
# Node ID a717c3dffe4fcb808e61fea4baec347236f0b796
# Parent  cc264a9a033dbefd118935f3e075453bf2fff93f
fixed spurious proof failure

diff -r cc264a9a033d -r a717c3dffe4f src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Feb 20 14:49:23 2009 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Feb 20 14:49:23 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