src/Pure/General/xml.ML

--- a/src/Pure/General/xml.ML	Wed Jul 13 22:05:55 2011 +0200
+++ b/src/Pure/General/xml.ML	Thu Jul 14 22:30:31 2011 +0200
@@ -293,9 +293,8 @@
 (* atomic values *)
 
 fun int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise XML_ATOM s);
+  Markup.parse_int s
+    handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
   | bool_atom "1" = true