src/Pure/ML/ml_syntax.ML
changeset 40626 d86540f6ea0d
parent 39514 d9cf3f833318
child 41415 23533273220a
--- 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;