diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 86439866e..4b6ced14a 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)
+local_context.cpp choice_iterator.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/choice_iterator.cpp b/src/frontends/lean/choice_iterator.cpp
new file mode 100644
index 000000000..1872216b6
--- /dev/null
+++ b/src/frontends/lean/choice_iterator.cpp
@@ -0,0 +1,27 @@
+/*
+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 "frontends/lean/choice_iterator.h"
+
+namespace lean {
+lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c, bool ignore_failure) {
+    return mk_lazy_list<constraints>([=]() {
+            auto s = c->next();
+            if (s) {
+                return some(mk_pair(*s, choose(c, false)));
+            } else if (ignore_failure) {
+                // return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable.
+                return lazy_list<constraints>::maybe_pair(constraints(), lazy_list<constraints>());
+            } else {
+                return lazy_list<constraints>::maybe_pair();
+            }
+        });
+}
+
+lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c) {
+    return choose(c, c->ignore_failure());
+}
+}
diff --git a/src/frontends/lean/choice_iterator.h b/src/frontends/lean/choice_iterator.h
new file mode 100644
index 000000000..59802ccd9
--- /dev/null
+++ b/src/frontends/lean/choice_iterator.h
@@ -0,0 +1,28 @@
+/*
+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 "util/lazy_list.h"
+#include "kernel/constraint.h"
+
+namespace lean {
+/** \brief Abstract (helper) class for creating lazy_list<constraints> */
+class choice_iterator {
+    bool m_ignore_failure;
+public:
+    choice_iterator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {}
+    virtual ~choice_iterator() {}
+    virtual optional<constraints> next() = 0;
+    bool ignore_failure() const { return m_ignore_failure; }
+};
+
+/** \brief Convert a choice_iterator into a lazy_list<constraints>
+    The lazy list is generated by invoking the method \c choice_iterator::next.
+    If c->ignore_failure() is true AND \c c does not produce any result,
+    then the singleton lazy_list is produced with an empty set of constraints.
+*/
+lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c);
+}
diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
index 8c09a44d9..07952aaf4 100644
--- a/src/frontends/lean/class.cpp
+++ b/src/frontends/lean/class.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 #include "library/opaque_hints.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/tactic_hint.h"
 
 namespace lean {
 struct class_entry {
@@ -151,4 +152,35 @@ void register_class_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
     add_cmd(r, cmd_info("class",    "add a new class", add_class_cmd));
 }
+
+/** \brief Return true iff \c type is a class or Pi that produces a class. */
+optional<name> is_ext_class(type_checker & tc, expr type) {
+    type = tc.whnf(type).first;
+    if (is_pi(type)) {
+        return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
+    } else {
+        expr f = get_app_fn(type);
+        if (!is_constant(f))
+            return optional<name>();
+        name const & cls_name = const_name(f);
+        if (is_class(tc.env(), cls_name) || !empty(get_tactic_hints(tc.env(), cls_name)))
+            return optional<name>(cls_name);
+        else
+            return optional<name>();
+    }
+}
+
+/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
+list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name) {
+    buffer<expr> buffer;
+    for (auto const & l : ctx) {
+        if (!is_local(l))
+            continue;
+        expr inst_type    = mlocal_type(l);
+        if (auto it = is_ext_class(tc, inst_type))
+            if (*it == cls_name)
+                buffer.push_back(l);
+    }
+    return to_list(buffer.begin(), buffer.end());
+}
 }
diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h
index f2851a095..9ccf9614d 100644
--- a/src/frontends/lean/class.h
+++ b/src/frontends/lean/class.h
@@ -21,4 +21,10 @@ bool is_class(environment const & env, name const & c);
 list<name> get_class_instances(environment const & env, name const & c);
 name get_class_name(environment const & env, expr const & e);
 void register_class_cmds(cmd_table & r);
+
+/** \brief Return true iff \c type is a class or Pi that produces a class. */
+optional<name> is_ext_class(type_checker & tc, expr type);
+
+/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
+list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name);
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index b10ec38ea..b913ae989 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/no_info.h"
 #include "frontends/lean/extra_info.h"
 #include "frontends/lean/local_context.h"
+#include "frontends/lean/choice_iterator.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -62,37 +63,6 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
     m_use_local_instances = get_elaborator_local_instances(ios.get_options());
 }
 
-/** \brief Return true iff \c type is a class or Pi that produces a class. */
-optional<name> is_ext_class(type_checker & tc, expr type) {
-    type = tc.whnf(type).first;
-    if (is_pi(type)) {
-        return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
-    } else {
-        expr f = get_app_fn(type);
-        if (!is_constant(f))
-            return optional<name>();
-        name const & cls_name = const_name(f);
-        if (is_class(tc.env(), cls_name) || !empty(get_tactic_hints(tc.env(), cls_name)))
-            return optional<name>(cls_name);
-        else
-            return optional<name>();
-    }
-}
-
-/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
-list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name) {
-    buffer<expr> buffer;
-    for (auto const & l : ctx) {
-        if (!is_local(l))
-            continue;
-        expr inst_type    = mlocal_type(l);
-        if (auto it = is_ext_class(tc, inst_type))
-            if (*it == cls_name)
-                buffer.push_back(l);
-    }
-    return to_list(buffer.begin(), buffer.end());
-}
-
 typedef std::unique_ptr<type_checker> type_checker_ptr;
 
 /** \brief Helper class for implementing the \c elaborate functions. */
@@ -162,19 +132,13 @@ class elaborator {
         }
     };
 
-    struct choice_elaborator {
-        bool m_ignore_failure;
-        choice_elaborator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {}
-        virtual optional<constraints> next() = 0;
-    };
-
     /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
         and a choice constraints <tt>(?m in fn)</tt> where \c fn is a choice function.
         The choice function produces a stream of alternatives. In this case, it produces a stream of
         size \c n, one alternative for each \c e_i.
         This is a helper class for implementing this choice functions.
     */
-    struct choice_expr_elaborator : public choice_elaborator {
+    struct choice_expr_elaborator : public choice_iterator {
         elaborator & m_elab;
         expr         m_mvar;
         expr         m_choice;
@@ -221,7 +185,7 @@ class elaborator {
 
         This is a helper class for implementing this choice function.
     */
-    struct placeholder_elaborator : public choice_elaborator {
+    struct placeholder_elaborator : public choice_iterator {
         elaborator &            m_elab;
         expr                    m_meta;
         expr                    m_meta_type; // elaborated type of the metavariable
@@ -238,7 +202,7 @@ class elaborator {
         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_elaborator(ignore_failure),
+            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);
@@ -337,20 +301,6 @@ class elaborator {
         }
     };
 
-    lazy_list<constraints> choose(std::shared_ptr<choice_elaborator> c) {
-        return mk_lazy_list<constraints>([=]() {
-                auto s = c->next();
-                if (s) {
-                    return some(mk_pair(*s, choose(c)));
-                } else if (c->m_ignore_failure) {
-                    // return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable.
-                    return lazy_list<constraints>::maybe_pair(constraints(), lazy_list<constraints>());
-                } else {
-                    return lazy_list<constraints>::maybe_pair();
-                }
-            });
-    }
-
 public:
     elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
         m_env(env),
@@ -453,36 +403,16 @@ public:
         m_pre_info_data.clear();
     }
 
-    static expr instantiate_meta(expr const & meta, substitution & subst) {
-        buffer<expr> locals;
-        expr mvar = get_app_args(meta, locals);
-        mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
-        for (auto & local : locals) local = subst.instantiate_all(local);
-        return ::lean::mk_app(mvar, locals);
-    }
-
-    /** \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(expr const & m) {
-        environment _env = env();
-        return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
-                substitution tmp(subst);
-                expr new_m    = instantiate_meta(m, tmp);
-                expr new_type = type_checker(_env).infer(new_m).first;
-                proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
-                return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
-            });
-    }
-
     /** \brief Create a metavariable, and attach choice constraint for generating
         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(m);
+        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 */) {
+        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;
@@ -633,7 +563,7 @@ public:
         return a;
     }
 
-    struct coercion_case_split {
+    struct coercion_case_split : public choice_iterator {
         elaborator &      m_elab;
         expr              m_arg;
         bool              m_id; // true if identity was not tried yet
@@ -662,21 +592,11 @@ public:
         }
     };
 
-    lazy_list<constraints> choose(std::shared_ptr<coercion_case_split> c) {
-        return mk_lazy_list<constraints>([=]() {
-                auto s = c->next();
-                if (s) {
-                    return some(mk_pair(*s, choose(c)));
-                } else {
-                    return lazy_list<constraints>::maybe_pair();
-                }
-            });
-    }
-
     constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type,
                                          justification const & j, unsigned delay_factor) {
         bool relax = m_relax_main_opaque;
-        auto choice_fn = [=](expr const & mvar, expr const & d_type, substitution const & s, name_generator const & /* ngen */) {
+        auto choice_fn = [=](expr const & mvar, expr const & d_type, substitution const & s,
+                             name_generator const & /* ngen */) {
             type_checker & tc = *m_tc[relax];
             expr          new_a_type;
             justification new_a_type_jst;
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index ef8c2c843..0709b934f 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -205,4 +205,24 @@ expr univ_metavars_to_params(environment const & env, local_decls<level> const &
                              name_set & ps, buffer<name> & new_ps, expr const & e) {
     return univ_metavars_to_params_fn(env, lls, s, ps, new_ps)(e);
 }
+
+expr instantiate_meta(expr const & meta, substitution & subst) {
+    lean_assert(is_meta(meta));
+    buffer<expr> locals;
+    expr mvar = get_app_args(meta, locals);
+    mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
+    for (auto & local : locals)
+        local = subst.instantiate_all(local);
+    return mk_app(mvar, locals);
+}
+
+justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
+    return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
+            substitution tmp(subst);
+            expr new_m    = instantiate_meta(m, tmp);
+            expr new_type = type_checker(env).infer(new_m).first;
+            proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
+            return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
+        });
+}
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index f59394126..be629f9cb 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -40,4 +40,11 @@ bool occurs(level const & u, level const & l);
 */
 expr univ_metavars_to_params(environment const & env, local_decls<level> const & lls, substitution & s,
                              name_set & ps, buffer<name> & new_ps, expr const & e);
+
+/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst  */
+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);
 }