src/HOL/Library/Univ_Poly.thy

--- a/src/HOL/Library/Univ_Poly.thy	Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 12 08:58:13 2010 +0200
@@ -71,7 +71,7 @@
 
 definition (in semiring_0)
   divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
-  [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+  "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
 
     --{*order of a polynomial*}
 definition (in ring_1) order :: "'a => 'a list => nat" where