src/Pure/General/yxml.ML

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