diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 24f811e8e..b7a6e711d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -265,15 +265,16 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     if (is_theorem) {
         if (p.num_threads() > 1) {
             // add as axiom, and create a task to prove the theorem
-            expr saved_type       = type;
-            expr saved_value      = value;
-            environment saved_env = env;
+            expr saved_type             = type;
+            expr saved_value            = value;
+            environment saved_env       = env;
+            local_level_decls saved_lls = p.get_local_level_decls();
             std::tie(type, new_ls) = p.elaborate_type(type);
             env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
             p.add_delayed_theorem([=, &p]() {
                     level_param_names new_ls;
                     expr type, value;
-                    std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, n, saved_type, saved_value);
+                    std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, saved_lls, n, saved_type, saved_value);
                     return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value));
                 });
         } else {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 262907d57..e13e43765 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -494,10 +494,10 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
     return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
 }
 
-std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, name const & n, expr const & t,
-                                                                          expr const & v) {
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
+                                                                          name const & n, expr const & t, expr const & v) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(env, m_local_level_decls, m_ios, n, t, v, &pp);
+    return ::lean::elaborate(env, lls, m_ios, n, t, v, &pp);
 }
 
 [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 3108b7232..73920f231 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -263,7 +263,7 @@ public:
     /** \brief Elaborate the definition n : t := v */
     std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
     /** \brief Elaborate the definition n : t := v in the given environment*/
-    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, name const & n, expr const & t, expr const & v);
+    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v);
 
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }