convenient printing of polynomial values

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