| changeset 38269 | cd6906d9199f |
| parent 38267 | e50c283dd125 |
| child 43698 | 91c4d7397f0e |
--- a/src/Pure/General/xml_data.ML Wed Aug 11 00:42:01 2010 +0200 +++ b/src/Pure/General/xml_data.ML Wed Aug 11 00:42:40 2010 +0200 @@ -78,9 +78,11 @@ | dest_properties ts = raise XML_BODY ts; -fun make_string s = [XML.Text s]; +fun make_string "" = [] + | make_string s = [XML.Text s]; -fun dest_string [XML.Text s] = s +fun dest_string [] = "" + | dest_string [XML.Text s] = s | dest_string ts = raise XML_BODY ts;