--- a/src/HOL/Int.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Int.thy Tue Apr 19 23:57:28 2011 +0200
@@ -2351,11 +2351,11 @@
fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
| strip_number_of t = t;
-fun numeral_codegen thy defs dep module b t gr =
+fun numeral_codegen thy mode defs dep module b t gr =
let val i = HOLogic.dest_numeral (strip_number_of t)
in
SOME (Codegen.str (string_of_int i),
- snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
+ snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
end handle TERM _ => NONE;
in