--- a/src/Pure/General/position.ML Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/General/position.ML Mon Mar 31 10:28:08 2014 +0200
@@ -166,7 +166,7 @@
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
-fun report_text pos markup txt = Output.report (reported_text pos markup txt);
+fun report_text pos markup txt = Output.report [reported_text pos markup txt];
fun report pos markup = report_text pos markup "";
type report = T * Markup.T;
@@ -174,7 +174,7 @@
val reports_text =
map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
- #> implode #> Output.report;
+ #> Output.report;
val reports = map (rpair "") #> reports_text;