--- a/src/Tools/Code/code_printer.ML Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Sat Jul 24 18:08:41 2010 +0200
@@ -39,7 +39,9 @@
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
- literal_numeral: int -> string, literal_positive_numeral: int -> string,
+ literal_numeral: int -> string,
+ literal_positive_numeral: int -> string,
+ literal_alternative_numeral: int -> string,
literal_naive_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
-> literals
@@ -47,6 +49,7 @@
val literal_string: literals -> string -> string
val literal_numeral: literals -> int -> string
val literal_positive_numeral: literals -> int -> string
+ val literal_alternative_numeral: literals -> int -> string
val literal_naive_numeral: literals -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
@@ -171,6 +174,7 @@
literal_string: string -> string,
literal_numeral: int -> string,
literal_positive_numeral: int -> string,
+ literal_alternative_numeral: int -> string,
literal_naive_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T,
infix_cons: int * string
@@ -182,6 +186,7 @@
val literal_string = #literal_string o dest_Literals;
val literal_numeral = #literal_numeral o dest_Literals;
val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
+val literal_alternative_numeral = #literal_alternative_numeral o dest_Literals;
val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;