src/Pure/General/xml.ML
changeset 43844 33e20b7d7e72
parent 43797 fad7758421bf
child 43947 9b00f09f7721
     1.1 --- a/src/Pure/General/xml.ML	Sat Jul 16 00:01:17 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Sat Jul 16 16:51:12 2011 +0200
     1.3 @@ -310,9 +310,10 @@
     1.4    | node t = raise XML_BODY [t];
     1.5  
     1.6  fun vector atts =
     1.7 -  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts;
     1.8 +  #1 (fold_map (fn (a, x) =>
     1.9 +        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
    1.10  
    1.11 -fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
    1.12 +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
    1.13    | tagged t = raise XML_BODY [t];
    1.14  
    1.15