| changeset 43781 | d43e5f79bdc2 |
| parent 43778 | ce9189450447 |
| child 43783 | ef45eaf2775f |
--- a/src/Pure/General/xml.ML Tue Jul 12 19:36:46 2011 +0200 +++ b/src/Pure/General/xml.ML Tue Jul 12 19:47:40 2011 +0200 @@ -307,7 +307,7 @@ val vector = fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a); -fun tagged (Elem ((name, props), ts)) = (int_atom name, (#1 (vector props 0), ts)) +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts)) | tagged t = raise XML_BODY [t];