parser: use plain explode, not Symbol.explode!

--- a/src/Pure/General/xml.ML	Thu Apr 03 23:38:59 2008 +0200
+++ b/src/Pure/General/xml.ML	Thu Apr 03 23:55:11 2008 +0200
@@ -169,7 +169,7 @@
 
 fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
-      (blanks |-- parse_element --| blanks))) (Symbol.explode s) of
+      (blanks |-- parse_element --| blanks))) (explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));