src/Pure/General/markup.ML
changeset 40131 7cbebd636e79
parent 39585 00be8711082f
child 40391 b0dafbfc05b7
--- a/src/Pure/General/markup.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/Pure/General/markup.ML	Mon Oct 25 20:24:13 2010 +0200
@@ -120,11 +120,11 @@
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
-  val no_output: output * output
-  val default_output: T -> output * output
-  val add_mode: string -> (T -> output * output) -> unit
-  val output: T -> output * output
-  val enclose: T -> output -> output
+  val no_output: Output.output * Output.output
+  val default_output: T -> Output.output * Output.output
+  val add_mode: string -> (T -> Output.output * Output.output) -> unit
+  val output: T -> Output.output * Output.output
+  val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
 end;