--- a/src/Pure/Isar/args.ML Fri Aug 04 23:00:01 2000 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 04 23:00:15 2000 +0200
@@ -25,6 +25,7 @@
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)
@@ -123,6 +124,7 @@
| _ => 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);