# HG changeset patch # User wenzelm # Date 955558023 -7200 # Node ID 24bff69370f0dc373c55bf9d67f4a17ac4962cfb # Parent 5893f2952e4fb0f6684db465d5771c817c23d71d Args.name_dummy; diff -r 5893f2952e4f -r 24bff69370f0 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Wed Apr 12 15:40:19 2000 +0200 +++ b/src/Pure/Isar/args.ML Wed Apr 12 18:47:03 2000 +0200 @@ -20,6 +20,7 @@ val !!! : (T list -> 'a) -> T list -> 'a val $$$ : string -> T list -> string * 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 var: T list -> indexname * T list val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) @@ -103,6 +104,7 @@ fun $$$ x = $$$$ x >> val_of; val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of; +val name_dummy = $$$ "_" >> K None || name >> Some; val keyword_symid = Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of; diff -r 5893f2952e4f -r 24bff69370f0 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Apr 12 15:40:19 2000 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Apr 12 18:47:03 2000 +0200 @@ -255,7 +255,7 @@ in read_instantiate context_of insts x thm end; val concl = Args.$$$ "concl" -- Args.$$$ ":"; -val inst_arg = Scan.unless concl (Args.$$$ "_" >> K None || Args.name >> Some); +val inst_arg = Scan.unless concl Args.name_dummy; val inst_args = Scan.repeat inst_arg; fun insts' x = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;