1.1 --- a/src/Tools/code/code_target.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -236,12 +236,12 @@
     1.4            else if c = c_bit1 then SOME 1
     1.5            else NONE
     1.6        | dest_bit _ = NONE;
     1.7 -    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0)
     1.8 -          else if c = c_min then SOME (IntInf.fromInt ~1)
     1.9 +    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
    1.10 +          else if c = c_min then SOME ~1
    1.11            else NONE
    1.12        | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
    1.13            if c = c_bit then case (dest_numeral t1, dest_bit t2)
    1.14 -           of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)
    1.15 +           of (SOME n, SOME b) => SOME (2 * n + b)
    1.16              | _ => NONE
    1.17            else NONE
    1.18        | dest_numeral _ = NONE;
    1.19 @@ -1631,15 +1631,15 @@
    1.20  val pretty : (string * {
    1.21      pretty_char: string -> string,
    1.22      pretty_string: string -> string,
    1.23 -    pretty_numeral: bool -> IntInf.int -> string,
    1.24 +    pretty_numeral: bool -> int -> string,
    1.25      pretty_list: Pretty.T list -> Pretty.T,
    1.26      infix_cons: int * string
    1.27    }) list = [
    1.28    ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
    1.29        pretty_string = ML_Syntax.print_string,
    1.30        pretty_numeral = fn unbounded => fn k =>
    1.31 -        if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
    1.32 -        else IntInf.toString k,
    1.33 +        if unbounded then "(" ^ string_of_int k ^ " : int)"
    1.34 +        else string_of_int k,
    1.35        pretty_list = Pretty.enum "," "[" "]",
    1.36        infix_cons = (7, "::")}),
    1.37    ("OCaml", { pretty_char = fn c => enclose "'" "'"
    1.38 @@ -1649,15 +1649,15 @@
    1.39              else c
    1.40            end),
    1.41        pretty_string = (fn _ => error "OCaml: no pretty strings"),
    1.42 -      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
    1.43 +      pretty_numeral = fn unbounded => fn k => if k >= 0 then
    1.44              if unbounded then
    1.45 -              "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
    1.46 -            else IntInf.toString k
    1.47 +              "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    1.48 +            else string_of_int k
    1.49            else
    1.50              if unbounded then
    1.51                "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
    1.52 -                o IntInf.toString o op ~) k ^ ")"
    1.53 -            else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
    1.54 +                o string_of_int o op ~) k ^ ")"
    1.55 +            else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
    1.56        pretty_list = Pretty.enum ";" "[" "]",
    1.57        infix_cons = (6, "::")}),
    1.58    ("Haskell", { pretty_char = fn c => enclose "'" "'"
    1.59 @@ -1667,10 +1667,8 @@
    1.60              else c
    1.61            end),
    1.62        pretty_string = ML_Syntax.print_string,
    1.63 -      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
    1.64 -            IntInf.toString k
    1.65 -          else
    1.66 -            (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
    1.67 +      pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    1.68 +          else enclose "(" ")" (signed_string_of_int k),
    1.69        pretty_list = Pretty.enum "," "[" "]",
    1.70        infix_cons = (5, ":")})
    1.71  ];