unused;

--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 13:20:37 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 13:25:58 2019 +0100
@@ -51,7 +51,6 @@
   val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
-  val output: tree -> BinIO.outstream -> unit
   val parse_comments: string list -> unit * string list
   val parse_string : string -> string option
   val parse_element: string list -> tree * string list
@@ -181,7 +180,6 @@
   in Buffer.empty |> traverse depth tree end;
 
 val string_of = Buffer.content o buffer_of ~1;
-val output = Buffer.output o buffer_of ~1;
 
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));