total Symbol.explode (cf. 1050315f6ee2);

--- a/src/Pure/ML/ml_syntax.ML	Fri Nov 19 21:14:12 2010 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Fri Nov 19 23:48:07 2010 +0100
@@ -104,7 +104,7 @@
     val str =
       implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
         handle Fail _ => raw_str;
-    val syms = Symbol.explode str handle ERROR _ => explode str;
+    val syms = Symbol.explode str;
   in Pretty.str (quote (implode (map print_char syms))) end;
 
 end;