# HG changeset patch
# User wenzelm
# Date 1207259711 -7200
# Node ID 5ee45391576e0b968423446ef29a5726e1cf53c3
# Parent  748631e95425b468eaa6c1b1d3a225ebddeb544c
parser: use plain explode, not Symbol.explode!

diff -r 748631e95425 -r 5ee45391576e src/Pure/General/xml.ML
--- 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));