diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3f557f108..b12e607ed 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -275,7 +275,7 @@ public:
         solutions using class-instances and tactic-hints.
     */
     expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
-        auto ec = mk_placeholder_elaborator(env(), ios(), m_context.get_data(),
+        auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
                                             m_ngen.next(), m_relax_main_opaque, use_local_instances(),
                                             is_strict, type, g, m_unifier_config);
         cs += ec.second;
diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
index 26721e969..0ee8a7f48 100644
--- a/src/frontends/lean/placeholder_elaborator.cpp
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -27,7 +27,7 @@ struct placeholder_context {
     local_context    m_ctx;
     bool             m_relax;
     bool             m_use_local_instances;
-    placeholder_context(environment const & env, io_state const & ios, list<expr> const & ctx,
+    placeholder_context(environment const & env, io_state const & ios, local_context const & ctx,
                         name const & prefix, bool relax, bool use_local_instances):
         m_ios(ios),
         m_ngen(prefix),
@@ -301,7 +301,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
     solutions using class-instances and tactic-hints.
 */
 pair<expr, constraint> mk_placeholder_elaborator(
-    environment const & env, io_state const & ios, list<expr> const & ctx,
+    environment const & env, io_state const & ios, local_context const & ctx,
     name const & prefix, bool relax, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg) {
     auto C       = std::make_shared<placeholder_context>(env, ios, ctx, prefix, relax, use_local_instances);
diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h
index bc0378f7b..63eb9dbe0 100644
--- a/src/frontends/lean/placeholder_elaborator.h
+++ b/src/frontends/lean/placeholder_elaborator.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/io_state.h"
+#include "frontends/lean/local_context.h"
 
 namespace lean {
 /** \brief Create a metavariable, and attach choice constraint for generating
@@ -24,7 +25,7 @@ namespace lean {
     \param tag  To be associated with new metavariables and expressions (for error localization).
 */
 pair<expr, constraint> mk_placeholder_elaborator(
-    environment const & env, io_state const & ios, list<expr> const & ctx,
+    environment const & env, io_state const & ios, local_context const & ctx,
     name const & prefix, bool relax_opaque, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg);
 }