--- a/src/Pure/General/xml.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/xml.ML Sat Nov 20 00:53:26 2010 +0100
@@ -158,7 +158,7 @@
val parse_comments =
blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
-val parse_string = Scan.read Symbol.stopper parse_chars o explode;
+val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
fun parse_content xs =
(parse_optional_text @@@
@@ -184,7 +184,7 @@
fun parse s =
(case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
- (blanks |-- parse_document --| blanks))) (explode s) of
+ (blanks |-- parse_document --| blanks))) (raw_explode s) of
(x, []) => x
| (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));