# HG changeset patch
# User wenzelm
# Date 1290206887 -3600
# Node ID d86540f6ea0d44d07fd833b38bc1c3d7d2890318
# Parent  2d9222a2239d429bafc3050db6a2942965401bcf
total Symbol.explode (cf. 1050315f6ee2);

diff -r 2d9222a2239d -r d86540f6ea0d src/Pure/ML/ml_syntax.ML
--- 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;