# HG changeset patch
# User wenzelm
# Date 1170622938 -3600
# Node ID 090f215ab631e34ae9fe119ef1da75448b91362c
# Parent  bb9b1c8a8a958eb38360e842b7b347658717398e
added print_strings;

diff -r bb9b1c8a8a95 -r 090f215ab631 src/Pure/General/ml_syntax.ML
--- 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;