diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index 281abb4b32..1b920d191f 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/io_state.h"
 namespace lean {
+unsigned get_default_priority(options const & opts);
 class parser;
 class decl_attributes {
 public:
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 52bbd9e3f0..f808fba39c 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -104,6 +104,7 @@ struct structure_cmd_fn {
     bool                        m_inductive_predicate;
     levels                      m_ctx_levels; // context levels for creating aliases
     buffer<expr>                m_ctx_locals; // context local constants for creating aliases
+    unsigned                    m_prio;
 
     structure_cmd_fn(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers):
         m_p(p),
@@ -115,6 +116,7 @@ struct structure_cmd_fn {
         m_explicit_universe_params = false;
         m_infer_result_universe    = false;
         m_inductive_predicate      = false;
+        m_prio                     = get_default_priority(p.get_options());
     }
 
     void check_attrs(decl_attributes const & attrs, pos_info const & pos) const {
@@ -817,7 +819,7 @@ struct structure_cmd_fn {
             if (!m_private_parents[i]) {
                 if (m_attrs.has_class() && is_class(m_env, parent_name)) {
                     // if both are classes, then we also mark coercion_name as an instance
-                    m_env = add_instance(m_env, coercion_name, LEAN_DEFAULT_PRIORITY, true);
+                    m_env = add_instance(m_env, coercion_name, m_prio, true);
                 }
             }
         }