1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Dec 23 18:37:51 2013 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Dec 23 20:45:33 2013 +0100
     1.3 @@ -367,8 +367,8 @@
     1.4  
     1.5  primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
     1.6  where
     1.7 -  "Poly [] = 0"
     1.8 -| "Poly (a # as) = pCons a (Poly as)"
     1.9 +  [code_post]: "Poly [] = 0"
    1.10 +| [code_post]: "Poly (a # as) = pCons a (Poly as)"
    1.11  
    1.12  lemma Poly_replicate_0 [simp]:
    1.13    "Poly (replicate n 0) = 0"