diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 4b6ced14a..b34ba6eaa 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -6,6 +6,6 @@ decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
 dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp
-local_context.cpp choice_iterator.cpp)
+local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d658489d1..d32d9b256 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -42,6 +42,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/extra_info.h"
 #include "frontends/lean/local_context.h"
 #include "frontends/lean/choice_iterator.h"
+#include "frontends/lean/placeholder_elaborator.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -63,8 +64,6 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
     m_use_local_instances = get_elaborator_local_instances(ios.get_options());
 }
 
-typedef std::unique_ptr<type_checker> type_checker_ptr;
-
 /** \brief Helper class for implementing the \c elaborate functions. */
 class elaborator {
     typedef name_map<expr> local_tactic_hints;
@@ -168,138 +167,6 @@ class elaborator {
         }
     };
 
-    /** \brief Whenever the elaborator finds a placeholder '_' or introduces an implicit argument, it creates
-        a metavariable \c ?m. It also creates a delayed choice constraint (?m in fn).
-
-        The function \c fn produces a stream of alternative solutions for ?m.
-        In this case, \c fn will do the following:
-          1) if the elaborated type of ?m is a 'class' C, then the stream will start with
-                  a) all local instances of class C (if elaborator.local_instances == true)
-                  b) solutions produced by tactic_hints for class C
-          2) if the elaborated type of ?m is not a class, then the stream will only contain
-             the solutions produced by tactic_hints.
-
-        The unifier only process delayed choice constraints when there are no other kind of constraint to be
-        processed.
-
-        This is a helper class for implementing this choice function.
-    */
-    struct placeholder_elaborator : public choice_iterator {
-        elaborator &            m_elab;
-        expr                    m_meta;
-        expr                    m_meta_type; // elaborated type of the metavariable
-        list<expr>              m_local_instances; // local instances that should also be included in the class-instance resolution.
-        list<name>              m_instances; // global declaration names that are class instances.
-                                             // This information is retrieved using #get_class_instances.
-        list<tactic_hint_entry> m_tactics;
-        proof_state_seq         m_tactic_result; // result produce by last executed tactic.
-        buffer<expr>            m_mvars_in_meta_type; // metavariables that occur in m_meta_type, the tactics may instantiate some of them
-        saved_state             m_state;
-        justification           m_jst;
-        bool                    m_relax_main_opaque;
-
-        placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type,
-                               list<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
-                               saved_state const & s, justification const & j, bool ignore_failure, bool relax):
-            choice_iterator(ignore_failure),
-            m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances),
-            m_tactics(tacs), m_state(s), m_jst(j), m_relax_main_opaque(relax) {
-            collect_metavars(meta_type, m_mvars_in_meta_type);
-        }
-
-        optional<constraints> try_instance(expr const & inst, expr const & inst_type) {
-            expr type   = inst_type;
-            // create the term pre (inst _ ... _)
-            expr pre    = copy_tag(m_meta, mk_explicit(inst));
-            while (true) {
-                type = m_elab.whnf(type).first;
-                if (!is_pi(type))
-                    break;
-                type = instantiate(binding_body(type), ::lean::mk_local(m_elab.m_ngen.next(), binding_domain(type)));
-                pre  = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder())));
-            }
-            try {
-                bool no_info = true;
-                new_scope s(m_elab, m_state, no_info);
-                expr type = m_meta_type;
-                buffer<expr> locals;
-                while (true) {
-                    type = m_elab.whnf(type).first;
-                    if (!is_pi(type))
-                        break;
-                    expr local  = ::lean::mk_local(m_elab.m_ngen.next(), binding_name(type), binding_domain(type),
-                                                   binding_info(type));
-                    if (binding_info(type).is_contextual())
-                        m_elab.m_context.add_local(local);
-                    m_elab.m_full_context.add_local(local);
-                    locals.push_back(local);
-                    type = instantiate(binding_body(type), local);
-                }
-                pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
-                expr r = Fun(locals, rcs.first);
-                buffer<constraint> cs;
-                to_buffer(rcs.second, m_jst, cs);
-                return optional<constraints>(cons(mk_eq_cnstr(m_meta, r, m_jst, m_relax_main_opaque),
-                                                  to_list(cs.begin(), cs.end())));
-            } catch (exception &) {
-                return optional<constraints>();
-            }
-        }
-
-        optional<constraints> try_instance(name const & inst) {
-            auto decl   = m_elab.env().find(inst);
-            if (!decl)
-                return optional<constraints>();
-            return try_instance(copy_tag(m_meta, mk_constant(inst)), decl->get_type());
-        }
-
-        optional<constraints> get_next_tactic_result() {
-            while (auto next = m_tactic_result.pull()) {
-                m_tactic_result = next->second;
-                if (!empty(next->first.get_goals()))
-                    continue; // has unsolved goals
-                substitution subst = next->first.get_subst();
-                buffer<constraint> cs;
-                expr const & mvar = get_app_fn(m_meta);
-                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
-                for (auto const & mvar : m_mvars_in_meta_type)
-                    cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
-                return optional<constraints>(to_list(cs.begin(), cs.end()));
-            }
-            return optional<constraints>();
-        }
-
-        virtual optional<constraints> next() {
-            while (!empty(m_local_instances)) {
-                expr inst         = head(m_local_instances);
-                m_local_instances = tail(m_local_instances);
-                if (!is_local(inst))
-                    continue;
-                if (auto r = try_instance(inst, mlocal_type(inst)))
-                    return r;
-            }
-            while (!empty(m_instances)) {
-                name inst   = head(m_instances);
-                m_instances = tail(m_instances);
-                if (auto cs = try_instance(inst))
-                    return cs;
-            }
-            if (auto cs = get_next_tactic_result())
-                return cs;
-            while (!empty(m_tactics)) {
-                tactic const & tac = head(m_tactics).get_tactic();
-                m_tactics          = tail(m_tactics);
-                proof_state ps(goals(goal(m_meta, m_meta_type)), substitution(), m_elab.m_ngen.mk_child());
-                try {
-                    m_tactic_result    = tac(m_elab.env(), m_elab.ios(), ps);
-                    if (auto cs = get_next_tactic_result())
-                        return cs;
-                } catch (exception &) {}
-            }
-            return optional<constraints>();
-        }
-    };
-
 public:
     elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
         m_env(env),
@@ -418,40 +285,11 @@ public:
         solutions using class-instances and tactic-hints.
     */
     expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
-        expr m              = m_context.mk_meta(type, g);
-        saved_state st(*this);
-        justification j     = mk_failed_to_synthesize_jst(env(), m);
-        bool relax          = m_relax_main_opaque;
-        auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
-                             name_generator const & /* ngen */) {
-            expr const & mvar = get_app_fn(meta);
-            if (auto cls_name_it = is_ext_class(*m_tc[relax], meta_type)) {
-                name cls_name = *cls_name_it;
-                list<expr> local_insts;
-                if (use_local_instances())
-                    local_insts = get_local_instances(*m_tc[relax], st.m_ctx, cls_name);
-                list<name>  insts = get_class_instances(env(), cls_name);
-                list<tactic_hint_entry> tacs;
-                if (!s.is_assigned(mvar))
-                    tacs = get_tactic_hints(env(), cls_name);
-                if (empty(local_insts) && empty(insts) && empty(tacs))
-                    return lazy_list<constraints>(); // nothing to be done
-                bool ignore_failure = false; // we are always strict with placeholders associated with classes
-                return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, local_insts, insts, tacs, st,
-                                                                       j, ignore_failure, m_relax_main_opaque));
-            } else if (s.is_assigned(mvar)) {
-                // if the metavariable is assigned and it is not a class, then we just ignore it, and return
-                // the an empty set of constraints.
-                return lazy_list<constraints>(constraints());
-            } else {
-                list<tactic_hint_entry> tacs = get_tactic_hints(env());
-                bool ignore_failure = !is_strict;
-                return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(),
-                                                                       tacs, st, j, ignore_failure, m_relax_main_opaque));
-            }
-        };
-        cs += mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance), false, j, m_relax_main_opaque);
-        return m;
+        auto ec = mk_placeholder_elaborator(env(), ios(), m_context.get_data(),
+                                            m_ngen.next(), m_relax_main_opaque, use_local_instances(),
+                                            is_strict, type, g);
+        cs += ec.second;
+        return ec.first;
     }
 
     expr visit_expecting_type(expr const & e, constraint_seq & cs) {
@@ -484,7 +322,8 @@ public:
         expr m              = m_full_context.mk_meta(t, e.get_tag());
         saved_state s(*this);
         bool relax          = m_relax_main_opaque;
-        auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & /* s */, name_generator const & /* ngen */) {
+        auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & /* s */,
+                      name_generator const & /* ngen */) {
             return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, s, relax));
         };
         justification j = mk_justification("none of the overloads is applicable", some_expr(e));
@@ -1014,16 +853,6 @@ public:
         return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), unifier_config(ios().get_options(), true));
     }
 
-    static void collect_metavars(expr const & e, buffer<expr> & mvars) {
-        for_each(e, [&](expr const & e, unsigned) {
-                if (is_metavar(e)) {
-                    mvars.push_back(e);
-                    return false; /* do not visit its type */
-                }
-                return has_metavar(e);
-            });
-    }
-
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) {
         lean_assert(is_metavar(mvar));
         if (!m_displayed_errors.contains(mlocal_name(mvar))) {
diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
new file mode 100644
index 000000000..a7b6c650a
--- /dev/null
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -0,0 +1,261 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "library/unifier.h"
+#include "library/opaque_hints.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/class.h"
+#include "frontends/lean/tactic_hint.h"
+#include "frontends/lean/local_context.h"
+#include "frontends/lean/choice_iterator.h"
+
+namespace lean {
+/** \brief Context for handling placeholder metavariable choice constraint */
+struct placeholder_context {
+    io_state         m_ios;
+    name_generator   m_ngen;
+    type_checker_ptr m_tc;
+    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,
+                        name const & prefix, bool relax, bool use_local_instances):
+        m_ios(ios),
+        m_ngen(prefix),
+        m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child(), relax)),
+        m_ctx(m_ngen.next(), ctx),
+        m_relax(relax),
+        m_use_local_instances(use_local_instances) {
+    }
+
+    environment const & env() const { return m_tc->env(); }
+    io_state const & ios() const { return m_ios; }
+    bool use_local_instances() const { return m_use_local_instances; }
+    type_checker & tc() const { return *m_tc; }
+};
+
+pair<expr, constraint> mk_placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
+                                                 bool is_strict, optional<expr> const & type, tag g);
+
+/** \brief Whenever the elaborator finds a placeholder '_' or introduces an
+    implicit argument, it creates a metavariable \c ?m. It also creates a
+    delayed choice constraint (?m in fn).
+
+    The function \c fn produces a stream of alternative solutions for ?m.
+    In this case, \c fn will do the following:
+    1) if the elaborated type of ?m is a 'class' C, then the stream will start with
+         a) all local instances of class C (if elaborator.local_instances == true)
+         b) solutions produced by tactic_hints for class C
+
+    2) if the elaborated type of ?m is not a class, then the stream will only contain
+       the solutions produced by tactic_hints.
+
+    The unifier only process delayed choice constraints when there are no other kind
+    of constraint to be processed.
+
+    This is a helper class for implementing this choice function.
+*/
+struct placeholder_elaborator : public choice_iterator {
+    std::shared_ptr<placeholder_context> m_C;
+    expr                    m_meta;
+    // elaborated type of the metavariable
+    expr                    m_meta_type;
+    // local instances that should also be included in the
+    // class-instance resolution.
+    // This information is retrieved from the local context
+    list<expr>              m_local_instances;
+    // global declaration names that are class instances.
+    // This information is retrieved using #get_class_instances.
+    list<name>              m_instances;
+    // Tactic hints for the class
+    list<tactic_hint_entry> m_tactics;
+    // result produce by last executed tactic.
+    proof_state_seq         m_tactic_result;
+    // metavariables that occur in m_meta_type, the tactics may instantiate some of them
+    buffer<expr>            m_mvars_in_meta_type;
+    justification           m_jst;
+
+    placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
+                           expr const & meta, expr const & meta_type,
+                           list<expr> const & local_insts, list<name> const & instances,
+                           list<tactic_hint_entry> const & tacs,
+                           justification const & j, bool ignore_failure):
+        choice_iterator(ignore_failure), m_C(C),
+        m_meta(meta), m_meta_type(meta_type),
+        m_local_instances(local_insts), m_instances(instances),
+        m_tactics(tacs),
+        m_jst(j) {
+        collect_metavars(meta_type, m_mvars_in_meta_type);
+    }
+
+    constraints mk_constraints(constraint const & c, buffer<constraint> const & cs) {
+        return cons(c, to_list(cs.begin(), cs.end()));
+    }
+
+    optional<constraints> try_instance(expr const & inst, expr const & inst_type) {
+        type_checker & tc     = m_C->tc();
+        name_generator & ngen = m_C->m_ngen;
+        tag g                 = inst.get_tag();
+        local_context & ctx   = m_C->m_ctx;
+        try {
+            local_context::scope scope(ctx);
+            buffer<expr> locals;
+            expr meta_type = m_meta_type;
+            while (true) {
+                meta_type = tc.whnf(meta_type).first;
+                if (!is_pi(meta_type))
+                    break;
+                expr local  = mk_local(ngen.next(), binding_name(meta_type),
+                                       binding_domain(meta_type), binding_info(meta_type));
+                ctx.add_local(local);
+                locals.push_back(local);
+                meta_type = instantiate(binding_body(meta_type), local);
+            }
+            expr type  = inst_type;
+            expr r     = inst;
+            buffer<constraint> cs;
+            while (true) {
+                type = tc.whnf(type).first;
+                if (!is_pi(type))
+                    break;
+                bool is_strict = true;
+                pair<expr, constraint> ac = mk_placeholder_elaborator(m_C, is_strict,
+                                                                      some_expr(binding_domain(type)), g);
+                expr arg = ac.first;
+                cs.push_back(ac.second);
+                r    = mk_app(r, arg).set_tag(g);
+                type = instantiate(binding_body(type), arg);
+            }
+            r = Fun(locals, r);
+            bool relax   = m_C->m_relax;
+            constraint c = mk_eq_cnstr(m_meta, r, m_jst, relax);
+            return optional<constraints>(mk_constraints(c, cs));
+        } catch (exception &) {
+            return optional<constraints>();
+        }
+    }
+
+    optional<constraints> try_instance(name const & inst) {
+        environment const & env = m_C->env();
+        if (auto decl = env.find(inst)) {
+            name_generator & ngen = m_C->m_ngen;
+            buffer<level> ls_buffer;
+            unsigned num_univ_ps = length(decl->get_univ_params());
+            for (unsigned i = 0; i < num_univ_ps; i++)
+                ls_buffer.push_back(mk_meta_univ(ngen.next()));
+            levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
+            expr inst_cnst = copy_tag(m_meta, mk_constant(inst, ls));
+            expr inst_type = instantiate_type_univ_params(*decl, ls);
+            return try_instance(inst_cnst, inst_type);
+        } else {
+            return optional<constraints>();
+        }
+    }
+
+    optional<constraints> get_next_tactic_result() {
+        while (auto next = m_tactic_result.pull()) {
+            m_tactic_result = next->second;
+            if (!empty(next->first.get_goals()))
+                continue; // has unsolved goals
+            substitution subst = next->first.get_subst();
+            buffer<constraint> cs;
+            expr const & mvar = get_app_fn(m_meta);
+            bool relax        = m_C->m_relax;
+            cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax));
+            for (auto const & mvar : m_mvars_in_meta_type)
+                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax));
+            return optional<constraints>(to_list(cs.begin(), cs.end()));
+        }
+        return optional<constraints>();
+    }
+
+    virtual optional<constraints> next() {
+        while (!empty(m_local_instances)) {
+            expr inst         = head(m_local_instances);
+            m_local_instances = tail(m_local_instances);
+            if (!is_local(inst))
+                continue;
+            if (auto r = try_instance(inst, mlocal_type(inst)))
+                return r;
+        }
+        while (!empty(m_instances)) {
+            name inst   = head(m_instances);
+            m_instances = tail(m_instances);
+            if (auto cs = try_instance(inst))
+                return cs;
+        }
+        if (auto cs = get_next_tactic_result())
+            return cs;
+        while (!empty(m_tactics)) {
+            tactic const & tac = head(m_tactics).get_tactic();
+            m_tactics          = tail(m_tactics);
+            proof_state ps(goals(goal(m_meta, m_meta_type)), substitution(), m_C->m_ngen.mk_child());
+            try {
+                m_tactic_result    = tac(m_C->env(), m_C->ios(), ps);
+                if (auto cs = get_next_tactic_result())
+                    return cs;
+            } catch (exception &) {}
+        }
+        return optional<constraints>();
+    }
+};
+
+
+pair<expr, constraint> mk_placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
+                                                 bool is_strict, optional<expr> const & type, tag g) {
+    expr m                  = C->m_ctx.mk_meta(type, g);
+    environment const & env = C->env();
+    justification j         = mk_failed_to_synthesize_jst(env, m);
+    auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
+                         name_generator const & /* ngen */) {
+        expr const & mvar = get_app_fn(meta);
+        if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) {
+            name cls_name = *cls_name_it;
+            list<expr> const & ctx = C->m_ctx.get_data();
+            list<expr> local_insts;
+            if (C->use_local_instances())
+                local_insts = get_local_instances(C->tc(), ctx, cls_name);
+            list<name>  insts = get_class_instances(env, cls_name);
+            list<tactic_hint_entry> tacs;
+            if (!s.is_assigned(mvar))
+                tacs = get_tactic_hints(env, cls_name);
+            if (empty(local_insts) && empty(insts) && empty(tacs))
+                return lazy_list<constraints>(); // nothing to be done
+            // we are always strict with placeholders associated with classes
+            bool ignore_failure = false;
+            return choose(std::make_shared<placeholder_elaborator>(C, meta, meta_type, local_insts, insts, tacs,
+                                                                   j, ignore_failure));
+        } else if (s.is_assigned(mvar)) {
+            // if the metavariable is assigned and it is not a class, then we just ignore it, and return
+            // the an empty set of constraints.
+            return lazy_list<constraints>(constraints());
+        } else {
+            list<tactic_hint_entry> tacs = get_tactic_hints(env);
+            bool ignore_failure = !is_strict;
+            return choose(std::make_shared<placeholder_elaborator>(C, meta, meta_type, list<expr>(), list<name>(),
+                                                                   tacs, j, ignore_failure));
+        }
+    };
+    bool owner      = false;
+    bool relax      = C->m_relax;
+    constraint c    = mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance),
+                                      owner, j, relax);
+    return mk_pair(m, c);
+}
+
+/** \brief Create a metavariable, and attach choice constraint for generating
+    solutions using class-instances and tactic-hints.
+*/
+pair<expr, constraint> mk_placeholder_elaborator(
+    environment const & env, io_state const & ios, list<expr> const & ctx,
+    name const & prefix, bool relax, bool use_local_instances,
+    bool is_strict, optional<expr> const & type, tag g) {
+    auto C = std::make_shared<placeholder_context>(env, ios, ctx, prefix, relax, use_local_instances);
+    return mk_placeholder_elaborator(C, is_strict, type, g);
+}
+}
diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h
new file mode 100644
index 000000000..d4ad1d9f2
--- /dev/null
+++ b/src/frontends/lean/placeholder_elaborator.h
@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+#include "library/io_state.h"
+
+namespace lean {
+/** \brief Create a metavariable, and attach choice constraint for generating
+    solutions using class-instances and tactic-hints.
+
+    \param ctx Local context where placeholder is located
+    \param prefix Prefix for metavariables that will be created by this procedure
+    \param relax True if opaque constants in the current module should be treated
+                 as transparent
+    \param use_local_instances If instances in the local context should be used
+                               in the class-instance resolution
+    \param is_strict True if constraint should fail if not solution is found,
+                     False if empty solution should be returned if there is no solution
+    \param type Expected type for the placeholder (if known)
+    \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,
+    name const & prefix, bool relax_opaque, bool use_local_instances,
+    bool is_strict, optional<expr> const & type, tag g);
+}
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 0709b934f..ffbf70f17 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/replace_fn.h"
+#include "kernel/for_each_fn.h"
 #include "library/scoped_ext.h"
 #include "library/locals.h"
 #include "library/explicit.h"
@@ -225,4 +226,14 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
             return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
         });
 }
+
+void collect_metavars(expr const & e, buffer<expr> & mvars) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_metavar(e)) {
+                mvars.push_back(e);
+                return false; /* do not visit its type */
+            }
+            return has_metavar(e);
+        });
+}
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index be629f9cb..bd07af5da 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -7,9 +7,11 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
+#include "kernel/type_checker.h"
 #include "frontends/lean/local_decls.h"
 namespace lean {
 class parser;
+typedef std::unique_ptr<type_checker> type_checker_ptr;
 void check_atomic(name const & n);
 void check_in_section_or_context(parser const & p);
 bool is_root_namespace(name const & n);
@@ -47,4 +49,8 @@ expr instantiate_meta(expr const & meta, substitution & subst);
 /** \brief Return a 'failed to synthesize placholder' justification for the given
     metavariable application \c m of the form (?m l_1 ... l_k) */
 justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
+
+/** \brief Copy the metavariables occurring in \c e to \c mvars,
+    this procedure ignores metavariables occurring in the type of metavariables. */
+void collect_metavars(expr const & e, buffer<expr> & mvars);
 }