--- a/src/Pure/General/ml_syntax.ML Sun Feb 04 22:02:17 2007 +0100
+++ b/src/Pure/General/ml_syntax.ML Sun Feb 04 22:02:18 2007 +0100
@@ -18,6 +18,7 @@
val print_option: ('a -> string) -> 'a option -> string
val print_char: string -> string
val print_string: string -> string
+ val print_strings: string list -> string
val print_class: class -> string
val print_sort: sort -> string
val print_typ: typ -> string
@@ -72,6 +73,7 @@
end;
val print_string = quote o translate_string print_char;
+val print_strings = print_list print_string;
val print_class = print_string;