src/Pure/General/yxml.ML
changeset 38474 e498dc2eb576
parent 38266 492d377ecfe2
child 42330 7a1655920fe8
     1.1 --- a/src/Pure/General/yxml.ML	Tue Aug 17 23:23:29 2010 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Wed Aug 18 11:02:47 2010 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  (* output *)
     1.5  
     1.6  fun output_markup (markup as (name, atts)) =
     1.7 -  if Markup.is_none markup then Markup.no_output
     1.8 +  if Markup.is_empty markup then Markup.no_output
     1.9    else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    1.10  
    1.11  fun element name atts body =