src/Pure/General/xml.ML
changeset 40131 7cbebd636e79
parent 39555 ccb223a4d49c
child 40627 becf5d5187cc
--- a/src/Pure/General/xml.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/xml.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -16,7 +16,7 @@
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
-  val output_markup: Markup.T -> output * output
+  val output_markup: Markup.T -> Output.output * Output.output
   val string_of: tree -> string
   val output: tree -> TextIO.outstream -> unit
   val parse_comments: string list -> unit * string list