--- a/src/HOL/Library/Polynomial.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy Thu Dec 29 10:47:56 2011 +0100
@@ -147,7 +147,7 @@
apply (rule le_degree, simp)
done
-lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
+lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
lemma pCons_eq_iff [simp]:
@@ -1505,8 +1505,6 @@
quickcheck_generator poly constructors: "0::'a::zero poly", pCons
-declare pCons_0_0 [code_post]
-
instantiation poly :: ("{zero, equal}") equal
begin