diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 480d07486..0ac0cbc04 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -20,9 +20,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 
 namespace lean {
-decl_attributes::decl_attributes(bool def_only, bool is_abbrev, bool persistent):
+decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
     m_priority() {
-    m_def_only               = def_only;
     m_is_abbrev              = is_abbrev;
     m_persistent             = persistent;
     m_is_instance            = false;
@@ -117,8 +116,6 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
             m_is_class = true;
             p.next();
         } else if (p.curr_is_token(get_multiple_instances_tk())) {
-            if (m_def_only)
-                throw parser_error("invalid '[multiple-instances]' attribute, only classes can have this attribute", pos);
             m_has_multiple_instances = true;
             p.next();
         } else if (auto it = parse_instance_priority(p)) {
@@ -246,7 +243,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
 }
 
 void decl_attributes::write(serializer & s) const {
-    s << m_def_only << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion
+    s << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion
       << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
       << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint
       << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
@@ -254,7 +251,7 @@ void decl_attributes::write(serializer & s) const {
 }
 
 void decl_attributes::read(deserializer & d) {
-    d >> m_def_only >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion
+    d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion
       >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
       >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint
       >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index 888d79f51..1a2164020 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 class decl_attributes {
-    bool               m_def_only; // if true only definition attributes are allowed
     bool               m_is_abbrev; // if true only abbreviation attributes are allowed
     bool               m_persistent;
     bool               m_is_instance;
@@ -38,7 +37,7 @@ class decl_attributes {
     void parse(name const & n, parser & p);
 
 public:
-    decl_attributes(bool def_only = true, bool is_abbrev = false, bool persistent = true);
+    decl_attributes(bool is_abbrev = false, bool persistent = true);
     void parse(buffer<name> const & ns, parser & p);
     void parse(parser & p);
     environment apply(environment env, io_state const & ios, name const & d) const;
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 48c3c2a7e..97a6dd3a1 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -1056,7 +1056,7 @@ public:
     definition_cmd_fn(parser & p, def_cmd_kind kind, bool is_private, bool is_protected):
         m_p(p), m_env(m_p.env()), m_kind(kind),
         m_is_private(is_private), m_is_protected(is_protected),
-        m_pos(p.pos()), m_attributes(true, kind == Abbreviation || kind == LocalAbbreviation) {
+        m_pos(p.pos()), m_attributes(kind == Abbreviation || kind == LocalAbbreviation) {
         lean_assert(!(m_is_private && m_is_protected));
     }
 
@@ -1183,9 +1183,8 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
     while (p.curr_is_identifier()) {
         ds.push_back(p.check_constant_next("invalid 'attribute' command, constant expected"));
     }
-    bool decl_only  = false;
     bool abbrev     = false;
-    decl_attributes attributes(decl_only, abbrev, persistent);
+    decl_attributes attributes(abbrev, persistent);
     attributes.parse(ds, p);
     environment env = p.env();
     for (name const & d : ds)