src/Pure/General/xml.ML
changeset 43783 ef45eaf2775f
parent 43781 d43e5f79bdc2
child 43791 5e9a1d71f94d
     1.1 --- a/src/Pure/General/xml.ML	Tue Jul 12 19:49:35 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Jul 12 20:11:00 2011 +0200
     1.3 @@ -304,8 +304,8 @@
     1.4  fun node (Elem ((":", []), ts)) = ts
     1.5    | node t = raise XML_BODY [t];
     1.6  
     1.7 -val vector =
     1.8 -  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a);
     1.9 +fun vector atts =
    1.10 +  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts;
    1.11  
    1.12  fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
    1.13    | tagged t = raise XML_BODY [t];