src/HOL/Integ/NatBin.thy
changeset 15965 f422f8283491
parent 15921 b6e345548913
child 16413 47ffc49c7d7b
     1.1 --- a/src/HOL/Integ/NatBin.thy	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -860,7 +860,7 @@
     1.4  ML {*
     1.5  fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
     1.6        Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
     1.7 -        (SOME (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin)))
     1.8 +        (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
     1.9          handle TERM _ => NONE)
    1.10    | number_of_codegen thy gr s b (Const ("Numeral.number_of",
    1.11        Type ("fun", [_, Type ("nat", [])])) $ bin) =