private void addAttribute(Annotations a, String ns, String localName, String prefix, String value, Token tok) {
    String key = ns + "#" + localName;
    if (attributeNameTable.get(key) != null)
      error("duplicate_attribute", ns, localName, tok);
    else {
      attributeNameTable.put(key, key);
      a.addAttribute(ns, localName, prefix, value, makeLocation(tok));
    }
  }