1.1 --- a/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -39,12 +39,15 @@
     1.4  
     1.5    type literals
     1.6    val Literals: { literal_char: string -> string, literal_string: string -> string,
     1.7 -        literal_numeral: bool -> int -> string,
     1.8 +        literal_numeral: int -> string, literal_positive_numeral: int -> string,
     1.9 +        literal_naive_numeral: int -> string,
    1.10          literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    1.11      -> literals
    1.12    val literal_char: literals -> string -> string
    1.13    val literal_string: literals -> string -> string
    1.14 -  val literal_numeral: literals -> bool -> int -> string
    1.15 +  val literal_numeral: literals -> int -> string
    1.16 +  val literal_positive_numeral: literals -> int -> string
    1.17 +  val literal_naive_numeral: literals -> int -> string
    1.18    val literal_list: literals -> Pretty.T list -> Pretty.T
    1.19    val infix_cons: literals -> int * string
    1.20  
    1.21 @@ -163,7 +166,9 @@
    1.22  datatype literals = Literals of {
    1.23    literal_char: string -> string,
    1.24    literal_string: string -> string,
    1.25 -  literal_numeral: bool -> int -> string,
    1.26 +  literal_numeral: int -> string,
    1.27 +  literal_positive_numeral: int -> string,
    1.28 +  literal_naive_numeral: int -> string,
    1.29    literal_list: Pretty.T list -> Pretty.T,
    1.30    infix_cons: int * string
    1.31  };
    1.32 @@ -173,6 +178,8 @@
    1.33  val literal_char = #literal_char o dest_Literals;
    1.34  val literal_string = #literal_string o dest_Literals;
    1.35  val literal_numeral = #literal_numeral o dest_Literals;
    1.36 +val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
    1.37 +val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
    1.38  val literal_list = #literal_list o dest_Literals;
    1.39  val infix_cons = #infix_cons o dest_Literals;
    1.40