src/Pure/Isar/args.ML

   val colon: T list -> string * T list
   val parens: (T list -> 'a * T list) -> T list -> 'a * T list
   val name: T list -> string * T list
   val name_dummy: T list -> string option * T list
   val nat: T list -> int * T list
+  val int: T list -> int * T list
   val var: T list -> indexname * T list
   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)

   (fn Arg (Ident, (x, _)) =>
     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   | _ => Scan.fail) >> #2;
 
 val nat = kind Syntax.read_nat;
+val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
 val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
 
 
 (* enumerations *)