# HG changeset patch
# User haftmann
# Date 1131437602 -3600
# Node ID 5d0243c9a302b1e361aff5e0cc6d4b6377b6e92e
# Parent  a36a9b2921e911d7a6c3ed5e8d0df965ba499d05
(fix for accidental commit)

diff -r a36a9b2921e9 -r 5d0243c9a302 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Nov 08 09:12:02 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Nov 08 09:13:22 2005 +0100
@@ -897,26 +897,19 @@
   "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, mk_int_to_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)))
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
 
-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)
-]*}
+setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
 
 quickcheck_params [default_type = int]