diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean
index b65bd5e20..9c7274d35 100644
--- a/hott/algebra/category/basic.hlean
+++ b/hott/algebra/category/basic.hlean
@@ -12,6 +12,8 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops
 structure category [class] (ob : Type) extends (precategory ob) :=
   (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
 
+multiple_instances [persistent] category
+
 namespace category
   variables {ob : Type} {C : category ob} {a b : ob}
   include C
diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 8c14eef4c..28eb10eda 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -14,6 +14,8 @@ structure precategory [class] (ob : Type) : Type :=
   (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
   (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
 
+multiple_instances [persistent] precategory
+
 namespace precategory
   variables {ob : Type} [C : precategory ob]
   variables {a b c d : ob}
diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean
index 6c853797a..2c36e8af7 100644
--- a/hott/algebra/precategory/morphism.hlean
+++ b/hott/algebra/precategory/morphism.hlean
@@ -16,6 +16,8 @@ namespace morphism
   inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
+  multiple_instances [persistent] is_iso
+
   definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
   definition section_of    (f : a ⟶ b) [H : is_retraction f] : hom b a :=
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index 81314fcd3..a87916c43 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -15,6 +15,8 @@ structure category [class] (ob : Type) : Type :=
   (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
   (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
 
+multiple_instances [persistent] category
+
 namespace category
   variables {ob : Type} [C : category ob]
   variables {a b c d : ob}
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 56a9d84b0..18bd0ac05 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -16,6 +16,8 @@ namespace morphism
   inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
+  multiple_instances [persistent] is_iso
+
   definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
   definition section_of    (f : a ⟶ b) [H : is_retraction f] : hom b a :=
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 333b48b1a..7c9e265f7 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -15,7 +15,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "instance" "class" "section" "fields" "find_decl"
+    "using" "namespace" "instance" "class" "multiple_instances" "section" "fields" "find_decl"
     "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
   "lean keywords")
 
diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
index 01532cf1e..7124a9c36 100644
--- a/src/frontends/lean/class.cpp
+++ b/src/frontends/lean/class.cpp
@@ -69,8 +69,24 @@ environment add_class_cmd(parser & p) {
     return env;
 }
 
+environment multiple_instances_cmd(parser & p) {
+    bool found = false;
+    environment env = p.env();
+    bool persistent = false;
+    parse_persistent(p, persistent);
+    while (p.curr_is_identifier()) {
+        found    = true;
+        name c   = p.check_constant_next("invalid 'multiple_instances' command, constant expected");
+        env = mark_multiple_instances(env, c, persistent);
+    }
+    if (!found)
+        throw parser_error("invalid 'multiple_instances' command, at least one identifier expected", p.pos());
+    return env;
+}
+
 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));
+    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));
+    add_cmd(r, cmd_info("multiple_instances", "mark that Lean must explore multiple instances of the given class", multiple_instances_cmd));
 }
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 8e9311c89..9d891c12d 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -91,7 +91,7 @@ void init_token_table(token_table & t) {
          "import", "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
-         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "find_decl",
+         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl",
          "include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =
diff --git a/src/library/class.cpp b/src/library/class.cpp
index a2fa659f9..ab2cd78ec 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -18,15 +18,18 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+enum class class_entry_kind { ClassCmd, InstanceCmd, MultiCmd };
 struct class_entry {
-    bool     m_class_cmd;
-    name     m_class;
-    name     m_instance; // only relevant if m_class_cmd == false
-    unsigned m_priority; // only relevant if m_class_cmd == false
-    class_entry():m_class_cmd(false), m_priority(0) {}
-    explicit class_entry(name const & c):m_class_cmd(true), m_class(c), m_priority(0) {}
+    class_entry_kind m_cmd_kind;
+    name             m_class;
+    name             m_instance; // only relevant if m_cmd_kind == InstanceCmd
+    unsigned         m_priority; // only relevant if m_cmd_kind == InstanceCmd
+    class_entry():m_cmd_kind(class_entry_kind::ClassCmd), m_priority(0) {}
+    explicit class_entry(name const & c):m_cmd_kind(class_entry_kind::ClassCmd), m_class(c), m_priority(0) {}
     class_entry(name const & c, name const & i, unsigned p):
-        m_class_cmd(false), m_class(c), m_instance(i), m_priority(p) {}
+        m_cmd_kind(class_entry_kind::InstanceCmd), m_class(c), m_instance(i), m_priority(p) {}
+    class_entry(name const & c, bool):
+        m_cmd_kind(class_entry_kind::MultiCmd), m_class(c) {}
 };
 
 struct class_state {
@@ -34,6 +37,7 @@ struct class_state {
     typedef name_map<unsigned>   instance_priorities;
     class_instances     m_instances;
     instance_priorities m_priorities;
+    name_set            m_multiple; // set of classes that allow multiple solutions/instances
 
     unsigned get_priority(name const & i) const {
         if (auto it = m_priorities.find(i))
@@ -42,6 +46,10 @@ struct class_state {
             return LEAN_INSTANCE_DEFAULT_PRIORITY;
     }
 
+    bool try_multiple_instances(name const & c) const {
+        return m_multiple.contains(c);
+    }
+
     list<name> insert(name const & inst, unsigned priority, list<name> const & insts) const {
         if (!insts)
             return to_list(inst);
@@ -68,6 +76,11 @@ struct class_state {
         if (p != LEAN_INSTANCE_DEFAULT_PRIORITY)
             m_priorities.insert(i, p);
     }
+
+    void add_multiple(name const & c) {
+        add_class(c);
+        m_multiple.insert(c);
+    }
 };
 
 static name * g_class_name = nullptr;
@@ -77,10 +90,17 @@ struct class_config {
     typedef class_state state;
     typedef class_entry entry;
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        if (e.m_class_cmd)
+        switch (e.m_cmd_kind) {
+        case class_entry_kind::ClassCmd:
             s.add_class(e.m_class);
-        else
+            break;
+        case class_entry_kind::InstanceCmd:
             s.add_instance(e.m_class, e.m_instance, e.m_priority);
+            break;
+        case class_entry_kind::MultiCmd:
+            s.add_multiple(e.m_class);
+            break;
+        }
     }
     static name const & get_class_name() {
         return *g_class_name;
@@ -89,25 +109,38 @@ struct class_config {
         return *g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
-        if (e.m_class_cmd)
-            s << true << e.m_class;
-        else
-            s << false << e.m_class << e.m_instance << e.m_priority;
+        s << static_cast<char>(e.m_cmd_kind);
+        switch (e.m_cmd_kind) {
+        case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
+            s << e.m_class;
+            break;
+        case class_entry_kind::InstanceCmd:
+            s << e.m_class << e.m_instance << e.m_priority;
+            break;
+        }
     }
     static entry read_entry(deserializer & d) {
-        entry e;
-        d >> e.m_class_cmd;
-        if (e.m_class_cmd)
+        entry e; char k;
+        d >> k;
+        e.m_cmd_kind = static_cast<class_entry_kind>(k);
+        switch (e.m_cmd_kind) {
+        case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
             d >> e.m_class;
-        else
+            break;
+        case class_entry_kind::InstanceCmd:
             d >> e.m_class >> e.m_instance >> e.m_priority;
+            break;
+        }
         return e;
     }
     static optional<unsigned> get_fingerprint(entry const & e) {
-        if (e.m_class_cmd)
+        switch (e.m_cmd_kind) {
+        case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
             return some(e.m_class.hash());
-        else
+        case class_entry_kind::InstanceCmd:
             return some(hash(hash(e.m_class.hash(), e.m_instance.hash()), e.m_priority));
+        }
+        lean_unreachable();
     }
 };
 
@@ -167,6 +200,16 @@ environment add_instance(environment const & env, name const & n, bool persisten
     return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent);
 }
 
+environment mark_multiple_instances(environment const & env, name const & n, bool persistent) {
+    check_class(env, n);
+    return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), persistent);
+}
+
+bool try_multiple_instances(environment const & env, name const & n) {
+    class_state const & s = class_ext::get_state(env);
+    return s.try_multiple_instances(n);
+}
+
 bool is_class(environment const & env, name const & c) {
     class_state const & s = class_ext::get_state(env);
     return s.m_instances.contains(c);
diff --git a/src/library/class.h b/src/library/class.h
index c17996b6e..9832cc3fa 100644
--- a/src/library/class.h
+++ b/src/library/class.h
@@ -21,6 +21,11 @@ list<name> get_class_instances(environment const & env, name const & c);
 void get_classes(environment const & env, buffer<name> & classes);
 name get_class_name(environment const & env, expr const & e);
 
+/** \brief Mark that multiple instances of class \c n must be explored. */
+environment mark_multiple_instances(environment const & env, name const & n, bool persistent);
+/** \brief Return true iff multiple instances of class \c n must be explored. */
+bool try_multiple_instances(environment const & env, name const & n);
+
 /** \brief Return true iff \c type is a class or Pi that produces a class. */
 optional<name> is_ext_class(type_checker & tc, expr const & type);
 
diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index 518f850a8..ec7a5e6e1 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -328,7 +328,9 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
 
     auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
                          name_generator const & ngen) {
-        if (!is_ext_class(C->tc(), meta_type)) {
+        environment const & env  = C->env();
+        auto cls_name_it = is_ext_class(C->tc(), meta_type);
+        if (!cls_name_it) {
             // do nothing, since type is not a class.
             return lazy_list<constraints>(constraints());
         }
@@ -342,7 +344,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
         new_cfg.m_discard        = false;
         new_cfg.m_use_exceptions = false;
 
-        auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) {
+        auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints {
             substitution new_s = subst;
             // some constraints may have been postponed (example: universe level constraints)
             constraints  postponed = map(cnstrs,
@@ -357,6 +359,13 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
             return append(cs, postponed);
         };
 
+        auto no_solution_fn = [=]() {
+            if (is_strict)
+                return lazy_list<constraints>();
+            else
+                return lazy_list<constraints>(constraints());
+        };
+
         unify_result_seq seq1    = unify(env, 1, &c, ngen, substitution(), new_cfg);
         if (get_class_unique_class_instances(C->m_ios.get_options())) {
             optional<expr> solution;
@@ -380,10 +389,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
                     }
                 });
             if (!solution) {
-                if (is_strict)
-                    return lazy_list<constraints>();
-                else
-                    return lazy_list<constraints>(constraints());
+                return no_solution_fn();
             } else {
                 // some constraints may have been postponed (example: universe level constraints)
                 return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs));
@@ -395,14 +401,22 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
                     // We only keep complete solutions (modulo universe metavariables)
                     return !has_expr_metavar_relaxed(result);
                 });
-            lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
-                    return to_cnstrs_fn(p.first, p.second);
-                });
-            if (is_strict) {
-                return seq3;
+            if (try_multiple_instances(env, *cls_name_it)) {
+                lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
+                        return to_cnstrs_fn(p.first, p.second);
+                    });
+                if (is_strict) {
+                    return seq3;
+                } else {
+                    // make sure it does not fail by appending empty set of constraints
+                    return append(seq3, lazy_list<constraints>(constraints()));
+                }
             } else {
-                // make sure it does not fail by appending empty set of constraints
-                return append(seq3, lazy_list<constraints>(constraints()));
+                auto p  = seq2.pull();
+                if (!p)
+                    return no_solution_fn();
+                else
+                    return lazy_list<constraints>(to_cnstrs_fn(p->first.first, p->first.second));
             }
         }
     };
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 144cd3818..a4d323106 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -50,6 +50,8 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom → 
     (rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
 rec_measure_aux default measure rec_val (succ (measure x)) x
 
+multiple_instances decidable
+
 theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
     (rec_val : dom → (dom → codom) → codom)
     (rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →