# HG changeset patch
# User huffman
# Date 1231889610 28800
# Node ID 4e08ee896e81816d259469a0cdf4f00defdbce62
# Parent  be8a15ffc511b16595dd5c4b3cdf88474a1ae466
declare pCons_0_0 [code post]

diff -r be8a15ffc511 -r 4e08ee896e81 src/HOL/Polynomial.thy
--- 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