src/Pure/General/markup.ML

--- a/src/Pure/General/markup.ML	Wed Jul 13 22:05:55 2011 +0200
+++ b/src/Pure/General/markup.ML	Thu Jul 14 22:30:31 2011 +0200
@@ -136,9 +136,11 @@
 (* integers *)
 
 fun parse_int s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise Fail ("Bad integer: " ^ quote s));
+  let val i = Int.fromString s in
+    if is_none i orelse String.isPrefix "~" s
+    then raise Fail ("Bad integer: " ^ quote s)
+    else the i
+  end;
 
 val print_int = signed_string_of_int;