src/Pure/General/xml.ML
changeset 43797 fad7758421bf
parent 43791 5e9a1d71f94d
child 43844 33e20b7d7e72
     1.1 --- a/src/Pure/General/xml.ML	Wed Jul 13 22:05:55 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Thu Jul 14 22:30:31 2011 +0200
     1.3 @@ -293,9 +293,8 @@
     1.4  (* atomic values *)
     1.5  
     1.6  fun int_atom s =
     1.7 -  (case Int.fromString s of
     1.8 -    SOME i => i
     1.9 -  | NONE => raise XML_ATOM s);
    1.10 +  Markup.parse_int s
    1.11 +    handle Fail _ => raise XML_ATOM s;
    1.12  
    1.13  fun bool_atom "0" = false
    1.14    | bool_atom "1" = true