src/Tools/Code/code_ml.ML
changeset 51143 0a2371e7ced3
parent 51091 c007c6bf4a35
child 52138 e21426f244aa
     1.1 --- a/src/Tools/Code/code_ml.ML	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -345,9 +345,6 @@
     1.4    literal_char = prefix "#" o quote o ML_Syntax.print_char,
     1.5    literal_string = quote o translate_string ML_Syntax.print_char,
     1.6    literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     1.7 -  literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     1.8 -  literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     1.9 -  literal_naive_numeral = string_of_int,
    1.10    literal_list = enum "," "[" "]",
    1.11    infix_cons = (7, "::")
    1.12  };
    1.13 @@ -693,9 +690,6 @@
    1.14    literal_char = Library.enclose "'" "'" o char_ocaml,
    1.15    literal_string = quote o translate_string char_ocaml,
    1.16    literal_numeral = numeral_ocaml,
    1.17 -  literal_positive_numeral = numeral_ocaml,
    1.18 -  literal_alternative_numeral = numeral_ocaml,
    1.19 -  literal_naive_numeral = numeral_ocaml,
    1.20    literal_list = enum ";" "[" "]",
    1.21    infix_cons = (6, "::")
    1.22  } end;