1.1 --- a/src/Pure/General/yxml.ML	Wed Apr 16 17:40:39 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Wed Apr 16 17:40:40 2008 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  (* parsing *)
     1.5  
     1.6  fun parse_attrib s =
     1.7 -  (case String.fields (is_char "=") s of
     1.8 +  (case space_explode "=" s of
     1.9      [] => err_attribute ()
    1.10    | "" :: _ => err_attribute ()
    1.11    | a :: xs => (a, space_implode "=" xs));