--- a/src/Tools/Code/code_ml.ML Fri Feb 15 08:31:30 2013 +0100
+++ b/src/Tools/Code/code_ml.ML Fri Feb 15 08:31:31 2013 +0100
@@ -345,9 +345,6 @@
literal_char = prefix "#" o quote o ML_Syntax.print_char,
literal_string = quote o translate_string ML_Syntax.print_char,
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
- literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
- literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
- literal_naive_numeral = string_of_int,
literal_list = enum "," "[" "]",
infix_cons = (7, "::")
};
@@ -693,9 +690,6 @@
literal_char = Library.enclose "'" "'" o char_ocaml,
literal_string = quote o translate_string char_ocaml,
literal_numeral = numeral_ocaml,
- literal_positive_numeral = numeral_ocaml,
- literal_alternative_numeral = numeral_ocaml,
- literal_naive_numeral = numeral_ocaml,
literal_list = enum ";" "[" "]",
infix_cons = (6, "::")
} end;