diff --git a/src/frontends/lean/old_attributes.cpp b/src/frontends/lean/old_attributes.cpp
index cbe868ea68..cbbaa46936 100644
--- a/src/frontends/lean/old_attributes.cpp
+++ b/src/frontends/lean/old_attributes.cpp
@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 void initialize_old_attributes() {
-    register_prio_attribute("elim", "elimination rule that is eagerly applied by blast grinder");
-    register_prio_attribute("intro!", "introduction rule that is eagerly applied by blast grinder");
-    register_no_params_attribute("no_pattern", "do not consider terms containing this declaration in the pattern inference procedure");
-    register_prio_attribute("forward", "forward chaining");
+    register_attribute(prio_attribute("elim", "elimination rule that is eagerly applied by blast grinder"));
+    register_attribute(prio_attribute("intro!", "introduction rule that is eagerly applied by blast grinder"));
+    register_attribute(basic_attribute("no_pattern", "do not consider terms containing this declaration in the pattern inference procedure"));
+    register_attribute(prio_attribute("forward", "forward chaining"));
 }
 void finalize_old_attributes() {}
 }
diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp
index f6525318e7..eddf31a7c8 100644
--- a/src/library/attribute_manager.cpp
+++ b/src/library/attribute_manager.cpp
@@ -7,36 +7,51 @@ Author: Leonardo de Moura
 #include <vector>
 #include <string>
 #include <algorithm>
+#include <unordered_map>
 #include "util/priority_queue.h"
 #include "util/sstream.h"
 #include "library/attribute_manager.h"
 #include "library/scoped_ext.h"
 
 namespace lean {
-struct attribute_decl {
-    std::string        m_id;
-    std::string        m_descr;
-    std::string        m_token;
-    set_attribute_proc m_on_set;
-};
 
-static std::vector<attribute_decl> * g_attr_decls;
+static std::unordered_map<std::string, attribute_ptr> * g_attributes;
 static std::vector<pair<std::string, std::string>> * g_incomp = nullptr;
 
 static std::string * g_key = nullptr;
 
+void register_attribute(attribute_ptr attr) {
+    lean_assert(!is_attribute(attr->get_name().c_str()));
+    (*g_attributes)[attr->get_name()] = attr;
+}
+
+bool is_attribute(std::string const & attr) {
+    return g_attributes->find(attr) != g_attributes->end();
+}
+
+[[ noreturn ]] void throw_unknown_attribute(std::string const & attr) {
+    throw exception(sstream() << "unknown attribute '" << attr << "'");
+}
+
+static attribute const & get_attribute(std::string const & attr) {
+    auto it = g_attributes->find(attr);
+    if (it != g_attributes->end())
+        return *it->second;
+    throw_unknown_attribute(attr);
+}
+
 struct attr_record {
-    name      m_decl;
-    list<unsigned> m_params;
+    name          m_decl;
+    attr_data_ptr m_data;
 
     attr_record() {}
-    attr_record(name decl, list<unsigned> params):
-            m_decl(decl), m_params(params) {}
+    attr_record(name decl, attr_data_ptr data):
+            m_decl(decl), m_data(data) {}
 
     unsigned hash() const {
         unsigned h = m_decl.hash();
-        for (unsigned p : m_params)
-            h = ::lean::hash(h, p);
+        if (m_data)
+            h = ::lean::hash(h, m_data->hash());
         return h;
     }
 };
@@ -49,12 +64,12 @@ struct attr_record_cmp {
 };
 
 struct attr_entry {
-    name     m_attr;
-    unsigned m_prio;
+    std::string m_attr;
+    unsigned    m_prio;
     attr_record m_record;
 
     attr_entry() {}
-    attr_entry(name attr, unsigned prio, attr_record record):
+    attr_entry(std::string const & attr, unsigned prio, attr_record const & record):
             m_attr(attr), m_prio(prio), m_record(record) {}
 };
 
@@ -76,102 +91,48 @@ struct attr_config {
     }
     static void write_entry(serializer & s, entry const & e) {
         s << e.m_attr << e.m_prio << e.m_record.m_decl;
-        write_list(s, e.m_record.m_params);
+        lean_assert(e.m_record.m_data);
+        get_attribute(e.m_attr).write_entry(s, *e.m_record.m_data);
     }
     static entry read_entry(deserializer & d) {
         entry e;
         d >> e.m_attr >> e.m_prio >> e.m_record.m_decl;
-        e.m_record.m_params = read_list<unsigned>(d);
+        e.m_record.m_data = get_attribute(e.m_attr).read_entry(d);
         return e;
     }
     static optional<unsigned> get_fingerprint(entry const & e) {
-        return optional<unsigned>(hash(hash(e.m_attr.hash(), e.m_record.hash()), e.m_prio));
+        return optional<unsigned>(hash(hash(name(e.m_attr).hash(), e.m_record.hash()), e.m_prio));
     }
 };
 
 template class scoped_ext<attr_config>;
 typedef scoped_ext<attr_config> attribute_ext;
 
-bool is_attribute(char const * attr) {
-    for (auto const & d : *g_attr_decls) {
-        if (d.m_id == attr)
-            return true;
-    }
-    return false;
+static attr_records const & get_attr_records(environment const & env, std::string const & n) {
+    if (auto state = attribute_ext::get_state(env).find(n))
+        return *state;
+    throw_unknown_attribute(n);
 }
 
-void register_attribute(char const * attr, char const * descr, set_attribute_proc const & on_set) {
-    lean_assert(!is_attribute(attr));
-    g_attr_decls->push_back(attribute_decl {attr, descr, std::string("[") + attr, on_set});
+environment attribute::set_core(environment const & env, io_state const & ios, name const & n, attr_data_ptr data,
+                                bool persistent) const {
+    return attribute_ext::add_entry(env, ios, attr_entry(m_id, LEAN_DEFAULT_PRIORITY, attr_record(n, data)), persistent);
 }
 
-void register_no_params_attribute(char const * attr, char const * descr, set_no_params_attribute_proc const & on_set) {
-    register_attribute(attr, descr,
-                       [=](environment const & env, io_state const & ios, name const & d, unsigned prio,
-                           list<unsigned> const & idxs, bool persistent) {
-                           if (prio != LEAN_DEFAULT_PRIORITY)
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, unexpected priority declaration");
-                           if (idxs)
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, unexpected parameter");
-                           return on_set(env, ios, d, persistent);
-                       });
-}
-void register_no_params_attribute(char const * attr, char const * descr) {
-    register_no_params_attribute(attr, descr,
-                                 [](environment const & env, io_state const &, name const &, bool) {
-                                     return env;
-                                 });
+environment basic_attribute::set(environment const & env, io_state const & ios, name const & n, bool persistent) const {
+    auto env2 = set_core(env, ios, n, attr_data_ptr(new attr_data), persistent);
+    if (m_on_set)
+        env2 = m_on_set(env2, ios, n, persistent);
+    return env2;
 }
 
-void register_prio_attribute(char const * attr, char const * descr, set_prio_attribute_proc const & on_set) {
-    register_attribute(attr, descr,
-                       [=](environment const & env, io_state const & ios, name const & d, unsigned prio,
-                          list<unsigned> const & idxs, bool persistent) {
-                           if (idxs)
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, unexpected parameter");
-                           return on_set(env, ios, d, prio, persistent);
-                       });
-}
-void register_prio_attribute(char const * attr, char const * descr) {
-    register_prio_attribute(attr, descr,
-                            [=](environment const & env, io_state const &, name const &, unsigned, bool) {
-                                return env;
-                            });
-}
-
-void register_opt_param_attribute(char const * attr, char const * descr, set_opt_param_attribute_proc const & on_set) {
-    register_attribute(attr, descr,
-                       [=](environment const & env, io_state const & ios, name const & d, unsigned prio,
-                          list<unsigned> const & idxs, bool persistent) {
-                           if (prio != LEAN_DEFAULT_PRIORITY)
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, unexpected priority declaration");
-                           if (idxs && tail(idxs))
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, expected at most one parameter");
-                           return on_set(env, ios, d, head_opt(idxs), persistent);
-                       });
-}
-
-void register_params_attribute(char const * attr, char const * descr, set_params_attribute_proc const & on_set) {
-    register_attribute(attr, descr,
-                       [=](environment const & env, io_state const & ios, name const & d, unsigned prio,
-                          list<unsigned> const & idxs, bool persistent) {
-                           if (prio != LEAN_DEFAULT_PRIORITY)
-                               throw exception(sstream() << "invalid [" << attr <<
-                                               "] declaration, unexpected priority declaration");
-                           return on_set(env, ios, d, idxs, persistent);
-                       });
-}
-void register_params_attribute(char const * attr, char const * descr) {
-    register_params_attribute(attr, descr,
-                              [=](environment const & env, io_state const &, name const &,
-                                  list<unsigned> const &, bool) {
-                                  return env;
-                              });
+environment prio_attribute::set(environment const & env, io_state const & ios, name const & n, unsigned prio,
+                                bool persistent) const {
+    auto env2 = attribute_ext::add_entry(env, ios, attr_entry(get_name(), prio, attr_record(n, attr_data_ptr(new attr_data))),
+                                         persistent);
+    if (m_on_set)
+        env2 = m_on_set(env2, ios, n, prio, persistent);
+    return env2;
 }
 
 void register_incompatible(char const * attr1, char const * attr2) {
@@ -185,34 +146,34 @@ void register_incompatible(char const * attr1, char const * attr2) {
 }
 
 void get_attributes(buffer<char const *> & r) {
-    for (auto const & d : *g_attr_decls)
-        r.push_back(d.m_id.c_str());
+    for (auto const & p : *g_attributes) {
+        r.push_back(p.second->get_name().c_str());
+    }
 }
 
 void get_attribute_tokens(buffer<char const *> & r) {
-    for (auto const & d : *g_attr_decls)
-        r.push_back(d.m_token.c_str());
+    for (auto const & p : *g_attributes) {
+        r.push_back(p.second->get_token().c_str());
+    }
 }
 
 char const * get_attribute_from_token(char const * tk) {
-    for (auto const & d : *g_attr_decls) {
-        if (d.m_token == tk)
-            return d.m_id.c_str();
+    if (*tk) {
+        // skip '['
+        if (is_attribute(tk + 1))
+            return get_attribute(tk + 1).get_name().c_str();
     }
     return nullptr;
 }
 
-char const * get_attribute_token(char const * attr) {
-    for (auto const & d : *g_attr_decls) {
-        if (d.m_id == attr)
-            return d.m_token.c_str();
-    }
-    return nullptr;
+char const * get_attribute_token(char const * name) {
+    return get_attribute(name).get_token().c_str();
 }
 
 bool has_attribute(environment const & env, char const * attr, name const & d) {
     if (auto it = attribute_ext::get_state(env).find(attr))
-        return it->contains(attr_record(d, list<unsigned>()));
+        // attr_data_ptr is ignored by comparison
+        return it->contains({d, {}});
     return false;
 }
 
@@ -226,40 +187,37 @@ priority_queue<name, name_quick_cmp> get_attribute_instances_by_prio(environment
     return q;
 }
 
-[[ noreturn ]] void throw_unknown_attribute(name const & attr) {
-    throw exception(sstream() << "unknown attribute '" << attr << "'");
-}
-
-environment set_attribute(environment const & env, io_state const & ios, char const * attr,
-                          name const & d, unsigned prio, list<unsigned> const & params, bool persistent) {
-    for (auto const & decl : *g_attr_decls) {
-        if (decl.m_id == attr) {
-            auto env2 = attribute_ext::add_entry(env, ios, attr_entry(attr, prio, attr_record(d, params)), persistent);
-            return decl.m_on_set(env2, ios, d, prio, params, persistent);
-        }
+environment set_attribute(environment const & env, io_state const & ios, char const * name,
+                          lean::name const & d, unsigned prio, list<unsigned> const & params, bool persistent) {
+    auto const & attr = get_attribute(name);
+    if (auto prio_attr = dynamic_cast<prio_attribute const *>(&attr)) {
+        lean_assert(!params);
+        return prio_attr->set(env, ios, d, prio, persistent);
     }
-    throw_unknown_attribute(attr);
-}
-
-environment set_attribute(environment const & env, io_state const & ios, char const * attr,
-                          name const & d, bool persistent) {
-    return set_attribute(env, ios, attr, d, LEAN_DEFAULT_PRIORITY, list<unsigned>(), persistent);
-}
-
-unsigned get_attribute_prio(environment const & env, name const & attr, name const & d) {
-    if (auto it = attribute_ext::get_state(env).find(attr)) {
-        optional<unsigned> prio = it->get_prio({d, list<unsigned>()});
-        return prio ? *prio : LEAN_DEFAULT_PRIORITY;
+    lean_assert(prio == LEAN_DEFAULT_PRIORITY);
+    if (auto params_attr = dynamic_cast<unsigned_params_attribute const *>(&attr)) {
+        return params_attr->set(env, ios, d, {params}, persistent);
     }
-    throw_unknown_attribute(attr);
+    lean_assert(!params);
+    return set_attribute(env, ios, name, d, persistent);
 }
 
-list<unsigned> get_attribute_params(environment const & env, name const & attr, name const & d) {
-    if (auto it = attribute_ext::get_state(env).find(attr)) {
-        if (auto record = it->get_key(attr_record {d, list<unsigned>()}))
-                return record->m_params;
-    }
-    throw_unknown_attribute(attr);
+environment set_attribute(environment const & env, io_state const & ios, char const * name, lean::name const & d,
+                          bool persistent) {
+    auto const & attr = get_attribute(name);
+    lean_assert(dynamic_cast<basic_attribute const *>(&attr));
+    return static_cast<basic_attribute const &>(attr).set(env, ios, d, persistent);
+}
+
+unsigned get_attribute_prio(environment const & env, std::string const & attr, name const & d) {
+    return get_attr_records(env, attr).get_prio({d, {}}).value();
+}
+
+list<unsigned> get_attribute_params(environment const & env, std::string const & attr, name const & d) {
+    auto record = get_attr_records(env, attr).get_key({d, {}});
+    lean_assert(record);
+    lean_assert(dynamic_cast<unsigned_params_attribute_data const *>(record->m_data.get()));
+    return static_cast<unsigned_params_attribute_data const *>(record->m_data.get())->m_params;
 }
 
 bool are_incompatible(char const * attr1, char const * attr2) {
@@ -271,7 +229,7 @@ bool are_incompatible(char const * attr1, char const * attr2) {
 }
 
 void initialize_attribute_manager() {
-    g_attr_decls = new std::vector<attribute_decl>();
+    g_attributes = new std::unordered_map<std::string, attribute_ptr>;
     g_incomp     = new std::vector<pair<std::string, std::string>>();
     g_key        = new std::string("ATTR");
     attribute_ext::initialize();
@@ -281,6 +239,7 @@ void finalize_attribute_manager() {
     attribute_ext::finalize();
     delete g_key;
     delete g_incomp;
-    delete g_attr_decls;
+    delete g_attributes;
 }
+
 }
diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h
index d8ca858251..047670537c 100644
--- a/src/library/attribute_manager.h
+++ b/src/library/attribute_manager.h
@@ -14,29 +14,130 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, list<unsigned> const &,
-                                  bool)> set_attribute_proc;
-typedef std::function<environment(environment const &, io_state const &, name const &,
-                                  bool)> set_no_params_attribute_proc;
-typedef std::function<environment(environment const &, io_state const &, name const &,
-                                  unsigned, bool)> set_prio_attribute_proc;
-typedef std::function<environment(environment const &, io_state const &, name const &,
-                                  optional<unsigned> const &, bool)> set_opt_param_attribute_proc;
-typedef std::function<environment(environment const &, io_state const &, name const &, list<unsigned> const &,
-                                  bool)> set_params_attribute_proc;
 
-void register_attribute(char const * attr, char const * descr, set_attribute_proc const & on_set);
-void register_no_params_attribute(char const * attr, char const * descr, set_no_params_attribute_proc const & on_set);
-void register_no_params_attribute(char const * attr, char const * descr);
-void register_prio_attribute(char const * attr, char const * descr, set_prio_attribute_proc const & on_set);
-void register_prio_attribute(char const * attr, char const * descr);
-void register_opt_param_attribute(char const * attr, char const * descr, set_opt_param_attribute_proc const & on_set);
-void register_params_attribute(char const * attr, char const * descr, set_params_attribute_proc const & on_set);
-void register_params_attribute(char const * attr, char const * descr);
+struct attr_data {
+    virtual unsigned hash() const {
+        return 0;
+    }
+};
+
+typedef std::shared_ptr<attr_data> attr_data_ptr;
+struct attr_config;
+
+class attribute {
+    friend struct attr_config;
+private:
+    std::string m_id;
+    std::string m_descr;
+    std::string m_token;
+protected:
+    environment set_core(environment const &, io_state const &, name const &, attr_data_ptr, bool) const;
+    virtual void write_entry(serializer &, attr_data const &) const = 0;
+    virtual attr_data_ptr read_entry(deserializer &) const = 0;
+public:
+    attribute(char const * id, char const * descr) : m_id(id), m_descr(descr), m_token(std::string("[") + id) {}
+    std::string const & get_name() const { return m_id; }
+    std::string const & get_token() const { return m_token; }
+};
+
+typedef std::shared_ptr<attribute const> attribute_ptr;
+
+/** \brief An attribute without associated data or priority declaration */
+class basic_attribute : public attribute {
+public:
+    typedef std::function<environment(environment const &, io_state const &, name const &, bool)> on_set_proc;
+private:
+    on_set_proc m_on_set;
+protected:
+    virtual void write_entry(serializer &, attr_data const &) const override final {}
+    virtual attr_data_ptr read_entry(deserializer &) const override final { return {}; }
+public:
+    basic_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
+                                                                               m_on_set(on_set) {}
+    basic_attribute(char const * id, char const * descr) : basic_attribute(id, descr, {}) {}
+    virtual environment set(environment const & env, io_state const & ios, name const & n, bool persistent) const;
+};
+
+// TODO(sullrich): Let the attribute handle priority parsing itself by introducing a custom
+// syntax (something like [attr:prio]?)
+class prio_attribute : public attribute {
+public:
+    typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, bool)> on_set_proc;
+private:
+    on_set_proc m_on_set;
+protected:
+    virtual void write_entry(serializer &, attr_data const &) const override final {}
+    virtual attr_data_ptr read_entry(deserializer &) const override final { return {}; }
+public:
+    prio_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
+                                                                              m_on_set(on_set) {}
+    prio_attribute(char const * id, char const * descr) : prio_attribute(id, descr, {}) {}
+    virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned prio,
+                            bool persistent) const;
+};
+
+template<typename Data>
+class typed_attribute : public attribute {
+public:
+    typedef std::function<environment(environment const &, io_state const &, name const &, Data const &, bool)>
+            on_set_proc;
+private:
+    on_set_proc m_on_set;
+protected:
+    virtual void write_entry(serializer & s, attr_data const & data) const final override {
+        lean_assert(dynamic_cast<Data const *>(&data));
+        static_cast<Data const &>(data).write(s);
+    }
+    virtual attr_data_ptr read_entry(deserializer & d) const final override {
+        auto data = new Data;
+        data->read(d);
+        return attr_data_ptr(data);
+    }
+public:
+    typed_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
+                                                                               m_on_set(on_set) {}
+    typed_attribute(char const * id, char const * descr) : typed_attribute(id, descr, {}) {}
+    virtual environment set(environment const & env, io_state const & ios, name const & n, Data const & data, bool persistent) const {
+        auto env2 = set_core(env, ios, n, std::unique_ptr<attr_data>(new Data(data)), persistent);
+        if (m_on_set)
+            env2 = m_on_set(env2, ios, n, data, persistent);
+        return env2;
+    }
+};
+
+struct unsigned_params_attribute_data : public attr_data {
+    list<unsigned> m_params;
+    unsigned_params_attribute_data(list<unsigned> const & params) : m_params(params) {}
+    unsigned_params_attribute_data() : unsigned_params_attribute_data(list<unsigned>()) {}
+
+    virtual unsigned hash() const override {
+        unsigned h = 0;
+        for (unsigned i : m_params)
+            h = ::lean::hash(h, i);
+        return h;
+    }
+    void write(serializer & s) const {
+        write_list(s, m_params);
+    }
+    void read(deserializer & d) {
+        m_params = read_list<unsigned>(d);
+    }
+};
+
+template class typed_attribute<unsigned_params_attribute_data>;
+typedef typed_attribute<unsigned_params_attribute_data> unsigned_params_attribute;
+
+void register_attribute(attribute_ptr);
+
+template<typename Attribute>
+void register_attribute(Attribute attr) {
+    register_attribute(attribute_ptr(new Attribute(attr)));
+}
 
 void register_incompatible(char const * attr1, char const * attr2);
 
-bool is_attribute(char const * attr);
+// TODO(sullrich): all of these should become members of/return attribute or a subclass
+bool is_attribute(std::string const & attr);
 void get_attributes(buffer<char const *> &);
 void get_attribute_tokens(buffer<char const *> &);
 char const * get_attribute_from_token(char const * attr_token);
@@ -51,8 +152,8 @@ bool has_attribute(environment const & env, char const * attr, name const & d);
 void get_attribute_instances(environment const & env, name const & attr, buffer<name> &);
 priority_queue<name, name_quick_cmp> get_attribute_instances_by_prio(environment const & env, name const & attr);
 
-unsigned get_attribute_prio(environment const & env, name const & attr, name const & d);
-list<unsigned> get_attribute_params(environment const & env, name const & attr, name const & d);
+unsigned get_attribute_prio(environment const & env, std::string const & attr, name const & d);
+list<unsigned> get_attribute_params(environment const & env, std::string const & attr, name const & d);
 
 bool are_incompatible(char const * attr1, char const * attr2);
 
diff --git a/src/library/class.cpp b/src/library/class.cpp
index d08869e17f..e69c7d90b8 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -422,20 +422,17 @@ void initialize_class() {
     g_key = new std::string("class");
     class_ext::initialize();
 
-    register_no_params_attribute("class", "type class",
-                                 [](environment const & env, io_state const &, name const & d, bool persistent) {
-                                     return add_class(env, d, persistent);
-                                 });
+    register_attribute(basic_attribute("class", "type class", [](environment const & env, io_state const &, name const & d, bool persistent) {
+          return add_class(env, d, persistent);
+        }));
 
-    register_prio_attribute("instance", "type class instance",
-                            [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
-                                return add_instance(env, d, prio, persistent);
-                            });
+    register_attribute(prio_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
+          return add_instance(env, d, prio, persistent);
+        }));
 
-    register_prio_attribute("trans_instance", "transitive type class instance",
-                            [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
-                                return add_trans_instance(env, d, prio, persistent);
-                            });
+    register_attribute(prio_attribute("trans_instance", "transitive type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
+          return add_trans_instance(env, d, prio, persistent);
+        }));
 }
 
 void finalize_class() {
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 52ebfff921..888028c65f 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -49,11 +49,9 @@ bool has_constructor_hint(environment const & env, name const & d) {
 }
 
 void initialize_normalize() {
-    register_params_attribute("unfold", "unfold definition when the given positions are constructors");
-    register_no_params_attribute("unfold_full",
-                                 "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied");
-    register_no_params_attribute("constructor",
-                                 "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator");
+    register_attribute(unsigned_params_attribute("unfold", "unfold definition when the given positions are constructors"));
+    register_attribute(basic_attribute("unfold_full", "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied"));
+    register_attribute(basic_attribute("constructor", "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator"));
 }
 
 void finalize_normalize() {
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index 1d33953d2a..395025ad19 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -15,9 +15,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 void initialize_reducible() {
-    register_no_params_attribute("reducible", "reducible");
-    register_no_params_attribute("semireducible", "semireducible");
-    register_no_params_attribute("irreducible", "irreducible");
+    register_attribute(basic_attribute("reducible", "reducible"));
+    register_attribute(basic_attribute("semireducible", "semireducible"));
+    register_attribute(basic_attribute("irreducible", "irreducible"));
 
     register_incompatible("reducible", "semireducible");
     register_incompatible("reducible", "irreducible");
diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp
index a96a6a1da1..b1311fec51 100644
--- a/src/library/relation_manager.cpp
+++ b/src/library/relation_manager.cpp
@@ -325,25 +325,21 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
 void initialize_relation_manager() {
     g_key       = new std::string("REL");
     rel_ext::initialize();
-    register_no_params_attribute("refl", "reflexive relation",
-                                 [](environment const & env, io_state const &, name const & d, bool persistent) {
-                                     return add_refl(env, d, persistent);
-                                 });
+    register_attribute(basic_attribute("refl", "reflexive relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
+          return add_refl(env, d, persistent);
+        }));
 
-    register_no_params_attribute("symm", "symmetric relation",
-                                 [](environment const & env, io_state const &, name const & d, bool persistent) {
-                                     return add_symm(env, d, persistent);
-                                 });
+    register_attribute(basic_attribute("symm", "symmetric relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
+          return add_symm(env, d, persistent);
+        }));
 
-    register_no_params_attribute("trans", "transitive relation",
-                                 [](environment const & env, io_state const &, name const & d, bool persistent) {
-                                     return add_trans(env, d, persistent);
-                                 });
+    register_attribute(basic_attribute("trans", "transitive relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
+          return add_trans(env, d, persistent);
+        }));
 
-    register_no_params_attribute("subst", "substitution",
-                                 [](environment const & env, io_state const &, name const & d, bool persistent) {
-                                     return add_subst(env, d, persistent);
-                                 });
+    register_attribute(basic_attribute("subst", "substitution", [](environment const & env, io_state const &, name const & d, bool persistent) {
+          return add_subst(env, d, persistent);
+        }));
 }
 
 void finalize_relation_manager() {
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index c3005adef9..d581191003 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -180,6 +180,7 @@ public:
         add_delayed_update([=](environment const & env, io_state const & ios) -> environment {
             return register_entry(env, ios, e);
         });
+
     }
     static state const & get_state(environment const & env) {
         return get(env).m_state;
diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp
index f40b517228..9d04be012b 100644
--- a/src/library/tactic/backward/backward_lemmas.cpp
+++ b/src/library/tactic/backward/backward_lemmas.cpp
@@ -132,15 +132,14 @@ vm_obj tactic_backward_lemmas_find(vm_obj const & lemmas, vm_obj const & h, vm_o
 
 void initialize_backward_lemmas() {
     register_trace_class(name{"tactic", "back_chaining"});
-    register_prio_attribute("intro", "introduction rule for backward chaining",
-                            [](environment const & env, io_state const & ios, name const & c, unsigned, bool) {
-                                aux_type_context ctx(env, ios.get_options());
-                                auto index = get_backward_target(ctx, c);
-                                if (!index || index->kind() != expr_kind::Constant)
-                                    throw exception(sstream() << "invalid [intro] attribute for '" << c
-                                                              << "', head symbol of resulting type must be a constant");
-                                return env;
-                            });
+    register_attribute(prio_attribute("intro", "introduction rule for backward chaining", [](environment const & env, io_state const & ios, name const & c, unsigned, bool) {
+          aux_type_context ctx(env, ios.get_options());
+          auto index = get_backward_target(ctx, c);
+          if (!index || index->kind() != expr_kind::Constant)
+            throw exception(sstream() << "invalid [intro] attribute for '" << c
+                            << "', head symbol of resulting type must be a constant");
+          return env;
+        }));
     DECLARE_VM_BUILTIN(name({"tactic", "mk_back_lemmas_core"}),      tactic_mk_backward_lemmas);
     DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_insert_core"}),  tactic_backward_lemmas_insert);
     DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_find"}),         tactic_backward_lemmas_find);
diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
index 359281abdb..5f72f81172 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
+++ b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
@@ -146,7 +146,7 @@ void initialize_defeq_simp_lemmas() {
 
     defeq_simp_lemmas_ext::initialize();
 
-    register_prio_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma);
+    register_attribute(prio_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma));
 }
 
 void finalize_defeq_simp_lemmas() {
diff --git a/src/library/tactic/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp
index 260b616b00..18cf8101a5 100644
--- a/src/library/tactic/simplifier/simp_lemmas.cpp
+++ b/src/library/tactic/simplifier/simp_lemmas.cpp
@@ -534,13 +534,13 @@ simp_lemmas get_simp_lemmas(type_context & tctx) {
     while (i > 0) {
         --i;
         tmp_type_context tmp_tctx(tctx);
-        r = add_core(tmp_tctx, r, simp_lemmas[i], get_attribute_prio(tctx.env(), get_simp_name(), simp_lemmas[i]));
+        r = add_core(tmp_tctx, r, simp_lemmas[i], get_attribute_prio(tctx.env(), "simp", simp_lemmas[i]));
     }
     i = congr_lemmas.size();
     while (i > 0) {
         --i;
         tmp_type_context tmp_tctx(tctx);
-        r = add_congr_core(tmp_tctx, r, congr_lemmas[i], get_attribute_prio(tctx.env(), get_congr_name(), congr_lemmas[i]));
+        r = add_congr_core(tmp_tctx, r, congr_lemmas[i], get_attribute_prio(tctx.env(), "congr", congr_lemmas[i]));
     }
     return r;
 }
@@ -586,8 +586,8 @@ void initialize_simp_lemmas() {
     DECLARE_VM_BUILTIN(name({"tactic", "mk_simp_lemmas_core"}),      tactic_mk_simp_lemmas);
     DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_core"}),  tactic_simp_lemmas_insert);
 
-    register_prio_attribute(get_simp_name().get_string(), "simplification lemma", on_add_simp_lemma);
-    register_prio_attribute(get_congr_name().get_string(), "congruence lemma", on_add_congr_lemma);
+    register_attribute(prio_attribute(get_simp_name().get_string(), "simplification lemma", on_add_simp_lemma));
+    register_attribute(prio_attribute(get_congr_name().get_string(), "congruence lemma", on_add_congr_lemma));
 }
 
 void finalize_simp_lemmas() {
diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp
index a7bc751a40..35f0838188 100644
--- a/src/library/unification_hint.cpp
+++ b/src/library/unification_hint.cpp
@@ -204,7 +204,7 @@ void initialize_unification_hint() {
 
     unification_hint_ext::initialize();
 
-    register_prio_attribute("unify", "unification hint", add_unification_hint);
+    register_attribute(prio_attribute("unify", "unification hint", add_unification_hint));
 }
 
 void finalize_unification_hint() {
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index bdbfbd5550..14cf09d8b5 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -344,10 +344,11 @@ has_recursors_pred::has_recursors_pred(environment const & env):
 void initialize_user_recursors() {
     g_key        = new std::string("UREC");
     recursor_ext::initialize();
-    register_opt_param_attribute("recursor", "user defined recursor",
-                                 [](environment const & env, io_state const &, name const & d, optional<unsigned> const & major, bool persistent) {
-                                     return add_user_recursor(env, d, major, persistent);
-                                 });
+    register_attribute(unsigned_params_attribute("recursor", "user defined recursor", [](environment const & env, io_state const &, name const & n, unsigned_params_attribute_data const & data, bool persistent) {
+          if (data.m_params && tail(data.m_params))
+            throw exception(sstream() << "invalid [recursor] declaration, expected at most one parameter");
+          return add_user_recursor(env, n, head_opt(data.m_params), persistent);
+        }));
 }
 
 void finalize_user_recursors() {