src/Pure/Isar/attrib.ML

 (
   type T = (((src -> attribute) * string) * stamp) NameSpace.table;
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
-  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
-    error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
+  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
+    error ("Attempt to merge different versions of attribute " ^ quote dup);
 );
 
 fun print_attributes thy =
   let
     val attribs = AttributesData.get thy;

 fun add_attributes raw_attrs thy =
   let
     val new_attrs =
       raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
     fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
-      handle Symtab.DUPS dups =>
-        error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
+      handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
   in AttributesData.map add thy end;
 
 
 
 (** attribute parsers **)
 
 (* tags *)
 
-fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x;
+fun tag x = Scan.lift (Args.name -- Args.name) x;
 
 
 (* theorems *)
 
 local