# HG changeset patch
# User haftmann
# Date 1443341474 -7200
# Node ID 0261eec37233e4f9c1259483e23e21eed255b97a
# Parent  542a4d9bac96dc0d721a3a3784e79fdd2c3b09ad
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

diff -r 542a4d9bac96 -r 0261eec37233 src/HOL/Code_Numeral.thy
--- 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"