1.1 --- a/src/Pure/General/pretty.ML	Tue Jun 22 09:51:51 2004 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Jun 22 09:51:59 2004 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4    val chunks: T list -> T
     1.5    val indent: int -> T -> T
     1.6    val string_of: T -> string
     1.7 +  val output: T -> string
     1.8    val writeln: T -> unit
     1.9    val writelns: T list -> unit
    1.10    val str_of: T -> string
    1.11 @@ -54,7 +55,6 @@
    1.12    val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    1.13    type pp
    1.14    val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
    1.15 -  val pp_undef: pp
    1.16    val term: pp -> term -> T
    1.17    val typ: pp -> typ -> T
    1.18    val sort: pp -> sort -> T
    1.19 @@ -240,10 +240,10 @@
    1.20  
    1.21  fun prune dp e = if dp > 0 then pruning dp e else e;
    1.22  
    1.23 -fun string_of e =
    1.24 -  Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty))
    1.25 -  |> Output.raw;
    1.26 +fun output e =
    1.27 +  Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
    1.28  
    1.29 +val string_of = Output.raw o output;
    1.30  val writeln = writeln o string_of;
    1.31  fun writelns [] = () | writelns es = writeln (chunks es);
    1.32  
    1.33 @@ -293,8 +293,4 @@
    1.34  val string_of_classrel = string_of oo classrel;
    1.35  val string_of_arity    = string_of oo arity;
    1.36  
    1.37 -fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
    1.38 -val pp_undef =
    1.39 -  pp (undef "term", undef "typ", undef "sort", undef "classrel", undef "arity");
    1.40 -
    1.41  end;