src/Pure/General/yxml.ML

--- a/src/Pure/General/yxml.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/yxml.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -52,7 +52,7 @@
 (* output *)
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then Markup.no_output
+  if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =