# HG changeset patch
# User haftmann
# Date 1131437522 -3600
# Node ID a36a9b2921e911d7a6c3ed5e8d0df965ba499d05
# Parent  fb76eea85835be455c1e01adf0649d7405390068
(codegen)

diff -r fb76eea85835 -r a36a9b2921e9 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Nov 08 02:19:11 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Nov 08 09:12:02 2005 +0100
@@ -897,19 +897,26 @@
   "neg"                         ("(_ < 0)")
 
 ML {*
+fun mk_int_to_nat bin =
+  Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
+  $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
+
 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
       Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
         (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
            Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE)
   | number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
       Type ("fun", [_, Type ("nat", [])])) $ bin) =
-        SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
-          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
+        SOME (Codegen.invoke_codegen thy defs s thyname b
+          (gr, mk_int_to_nat bin))
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
 
-setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
+setup {*[
+  Codegen.add_codegen "number_of_codegen" number_of_codegen,
+  CodegenPackage.add_codegen_expr
+    ("number", CodegenPackage.codegen_number_of HOLogic.dest_binum mk_int_to_nat)
+]*}
 
 quickcheck_params [default_type = int]