made SML/NJ happy;
authorwenzelm
Tue Jul 12 20:11:00 2011 +0200 (2011-07-12)
changeset 43783ef45eaf2775f
parent 43782 834de29572d5
child 43784 c3b6374278fa
made SML/NJ happy;
src/Pure/General/xml.ML
     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];