--- a/src/HOL/Polynomial.thy Tue Jan 13 14:08:24 2009 -0800
+++ b/src/HOL/Polynomial.thy Tue Jan 13 15:33:30 2009 -0800
@@ -1024,6 +1024,8 @@
code_datatype "0::'a::zero poly" pCons
+declare pCons_0_0 [code post]
+
instantiation poly :: ("{zero,eq}") eq
begin