--- a/src/Tools/Code/code_printer.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_printer.ML Tue Apr 24 14:17:58 2018 +0000
@@ -39,11 +39,10 @@
val aux_params: var_ctxt -> iterm list list -> string list
type literals
- val Literals: { literal_char: string -> string, literal_string: string -> string,
+ val Literals: { literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
-> literals
- val literal_char: literals -> string -> string
val literal_string: literals -> string -> string
val literal_numeral: literals -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
@@ -215,7 +214,6 @@
(** pretty literals **)
datatype literals = Literals of {
- literal_char: string -> string,
literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T,
@@ -224,7 +222,6 @@
fun dest_Literals (Literals lits) = lits;
-val literal_char = #literal_char o dest_Literals;
val literal_string = #literal_string o dest_Literals;
val literal_numeral = #literal_numeral o dest_Literals;
val literal_list = #literal_list o dest_Literals;