# HG changeset patch
# User berghofe
# Date 1127296976 -7200
# Node ID 2a747fc49a8c45dc947cd47099a4636a27c5f96f
# Parent  9bcd6ea262b839e66ec9a37cac3cc8cdee725859
Simplified code generator for numerals.

diff -r 9bcd6ea262b8 -r 2a747fc49a8c src/HOL/Integ/IntDef.thy
--- 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;
 *}