src/Pure/ML/ml_syntax.ML
changeset 40626 d86540f6ea0d
parent 39514 d9cf3f833318
child 41415 23533273220a
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Fri Nov 19 21:14:12 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Fri Nov 19 23:48:07 2010 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4      val str =
     1.5        implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
     1.6          handle Fail _ => raw_str;
     1.7 -    val syms = Symbol.explode str handle ERROR _ => explode str;
     1.8 +    val syms = Symbol.explode str;
     1.9    in Pretty.str (quote (implode (map print_char syms))) end;
    1.10  
    1.11  end;