# HG changeset patch
# User berghofe
# Date 1127816079 -7200
# Node ID 2beb71c0f92e4b1e4166dc3444e1aab894d01095
# Parent  4708ab4626a53c171bc29b18f86d531106df9367
Inserted clause for nat in number_of_codegen again ("code unfold" turned
out to be too inefficient).

diff -r 4708ab4626a5 -r 2beb71c0f92e src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Sep 27 12:13:17 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue Sep 27 12:14:39 2005 +0200
@@ -901,6 +901,11 @@
       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)))
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}