Args.name_dummy;

--- 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;

--- 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;