more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

--- a/src/HOL/Code_Numeral.thy	Mon Sep 28 17:29:01 2015 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Sep 27 10:11:14 2015 +0200
@@ -244,12 +244,18 @@
 
 definition Pos :: "num \<Rightarrow> integer"
 where
-  [simp, code_abbrev]: "Pos = numeral"
+  [simp, code_post]: "Pos = numeral"
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer numeral Pos"
   by simp transfer_prover
 
+lemma Pos_fold [code_unfold]:
+  "numeral Num.One = Pos Num.One"
+  "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
+  "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"
+  by simp_all
+
 definition Neg :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Neg n = - Pos n"