--- a/src/Pure/General/graph_display.ML Mon Jan 19 21:15:30 2015 +0100
+++ b/src/Pure/General/graph_display.ML Mon Jan 19 21:24:47 2015 +0100
@@ -88,7 +88,7 @@
YXML.output_markup_elem
(Active.make_markup Markup.graphviewN {implicit = false, properties = []});
val _ =
- writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "new graph" ^ en);
+ writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
val ((bg1, bg2), en) =
YXML.output_markup_elem