src/HOL/Integ/IntDef.thy

--- a/src/HOL/Integ/IntDef.thy	Fri Dec 02 16:04:48 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Dec 02 16:05:12 2005 +0100
@@ -915,8 +915,8 @@
 
 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)
+  CodegenPackage.add_appgen
+    ("number", CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat)
 ]*}
 
 quickcheck_params [default_type = int]