src/HOL/Int.thy
changeset 42411 ff997038e8eb
parent 41959 b460124855b8
child 42676 8724f20bf69c
     1.1 --- a/src/HOL/Int.thy	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -2351,11 +2351,11 @@
     1.4  fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
     1.5    | strip_number_of t = t;
     1.6  
     1.7 -fun numeral_codegen thy defs dep module b t gr =
     1.8 +fun numeral_codegen thy mode defs dep module b t gr =
     1.9    let val i = HOLogic.dest_numeral (strip_number_of t)
    1.10    in
    1.11      SOME (Codegen.str (string_of_int i),
    1.12 -      snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
    1.13 +      snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
    1.14    end handle TERM _ => NONE;
    1.15  
    1.16  in