diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Int.thy	Thu Oct 09 08:47:27 2008 +0200
@@ -1969,11 +1969,11 @@
 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
   | strip_number_of t = t;
 
-fun numeral_codegen thy defs gr dep module b t =
+fun numeral_codegen thy defs dep module b t gr =
   let val i = HOLogic.dest_numeral (strip_number_of t)
   in
-    SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
-      Codegen.str (string_of_int i))
+    SOME (Codegen.str (string_of_int i),
+      snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
   end handle TERM _ => NONE;
 
 in