Simplified code generator for numerals.

--- a/src/HOL/Integ/IntDef.thy	Wed Sep 21 12:02:19 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Sep 21 12:02:56 2005 +0200
@@ -897,15 +897,10 @@
   "neg"                         ("(_ < 0)")
 
 ML {*
-fun number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
-        (SOME (gr, 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)))
+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 _ _ _ _ _ _ _ = NONE;
 *}