# HG changeset patch
# User berghofe
# Date 1189072397 -7200
# Node ID 98c978a42a42f4df0e489b4005e96a2ca2a3a7fc
# Parent  68dab042dea89e18d896319ceac195bb95311a8a
Generalized code generator for numerals.

diff -r 68dab042dea8 -r 98c978a42a42 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Thu Sep 06 11:52:13 2007 +0200
+++ b/src/HOL/Numeral.thy	Thu Sep 06 11:53:17 2007 +0200
@@ -649,25 +649,25 @@
 setup {*
 let
 
-fun number_of_codegen thy defs gr dep module b (Const (@{const_name Numeral.number_of}, Type ("fun", [_, T])) $ t) =
-      if T = HOLogic.intT then
-        (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
-          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
-      else if T = HOLogic.natT then
-        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
-          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const (@{const_name Numeral.number_of}, HOLogic.intT --> HOLogic.intT) $ t)))
-      else NONE
-  | number_of_codegen _ _ _ _ _ _ _ = NONE;
+fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
+  | strip_number_of t = t;
+
+fun numeral_codegen thy defs gr dep module b t =
+  let val i = HOLogic.dest_numeral (strip_number_of t)
+  in
+    SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
+      Pretty.str (IntInf.toString i))
+  end handle TERM _ => NONE;
 
 in
 
-Codegen.add_codegen "number_of_codegen" number_of_codegen
+Codegen.add_codegen "numeral_codegen" numeral_codegen
 
 end
 *}
 
 consts_code
+  "number_of :: int \<Rightarrow> int"    ("(_)")
   "0 :: int"                   ("0")
   "1 :: int"                   ("1")
   "uminus :: int => int"       ("~")