1.1 --- a/src/Pure/General/yxml.ML	Wed Aug 27 16:32:18 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Wed Aug 27 16:32:48 2008 +0200
     1.3 @@ -101,10 +101,10 @@
     1.4  (* parsing *)
     1.5  
     1.6  fun parse_attrib s =
     1.7 -  (case space_explode "=" s of
     1.8 -    [] => err_attribute ()
     1.9 -  | "" :: _ => err_attribute ()
    1.10 -  | a :: xs => (a, space_implode "=" xs));
    1.11 +  (case find_substring "=" s of
    1.12 +    NONE => err_attribute ()
    1.13 +  | SOME 0 => err_attribute ()
    1.14 +  | SOME i => (String.substring (s, 0, i), String.extract (s, i + 1, NONE)));
    1.15  
    1.16  fun parse_chunk ["", ""] = pop
    1.17    | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)