1.1 --- a/src/Pure/General/pretty.ML	Sat Dec 08 14:42:22 2001 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Dec 08 14:42:45 2001 +0100
     1.3 @@ -46,6 +46,7 @@
     1.4    val indent: int -> T -> T
     1.5    val string_of: T -> string
     1.6    val writeln: T -> unit
     1.7 +  val writelns: T list -> unit
     1.8    val str_of: T -> string
     1.9    val pprint: T -> pprint_args -> unit
    1.10    val setdepth: int -> unit
    1.11 @@ -223,6 +224,7 @@
    1.12  
    1.13  fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
    1.14  val writeln = writeln o string_of;
    1.15 +fun writelns [] = () | writelns es = writeln (chunks es);
    1.16  
    1.17  
    1.18  (*Create a single flat string: no line breaking*)