# HG changeset patch
# User berghofe
# Date 1078092348 -3600
# Node ID 34ffa53db76ca68f3b2ea72ddafe5ceef1c53d83
# Parent  1f256287d4f0f364b7c511f2eb6859aada3f350b
Added specific code generator for number_of.

diff -r 1f256287d4f0 -r 34ffa53db76c src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Feb 26 17:08:23 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy	Sun Feb 29 23:05:48 2004 +0100
@@ -841,4 +841,19 @@
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")
 
+ML {*
+fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
+      Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
+        (Some (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin)))
+        handle TERM _ => None)
+  | number_of_codegen thy gr s b (Const ("Numeral.number_of",
+      Type ("fun", [_, Type ("nat", [])])) $ bin) =
+        Some (Codegen.invoke_codegen thy s 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] *}
+
 end