diff --git a/src/library/class_instance_synth.cpp b/src/library/class_instance_synth.cpp
index 03475b754..5f643ce6e 100644
--- a/src/library/class_instance_synth.cpp
+++ b/src/library/class_instance_synth.cpp
@@ -45,6 +45,7 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+static name * g_tmp_prefix                   = nullptr;
 static name * g_class_unique_class_instances = nullptr;
 static name * g_class_trace_instances        = nullptr;
 static name * g_class_instance_max_depth     = nullptr;
@@ -55,6 +56,7 @@ static name * g_class_trans_instances        = nullptr;
 [[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); }
 
 void initialize_class_instance_elaborator() {
+    g_tmp_prefix                   = new name(name::mk_internal_unique_name());
     g_class_unique_class_instances = new name{"class", "unique_instances"};
     g_class_trace_instances        = new name{"class", "trace_instances"};
     g_class_instance_max_depth     = new name{"class", "instance_max_depth"};
@@ -79,6 +81,7 @@ void initialize_class_instance_elaborator() {
 }
 
 void finalize_class_instance_elaborator() {
+    delete g_tmp_prefix;
     delete g_class_unique_class_instances;
     delete g_class_trace_instances;
     delete g_class_instance_max_depth;
@@ -514,6 +517,10 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
     return mk_class_instance(env, ios, lctx, prefix, type, use_local_instances, cfg);
 }
 
+optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type) {
+    return mk_class_instance(env, get_dummy_ios(), ctx, *g_tmp_prefix, type);
+}
+
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
     level lvl        = sort_level(tc.ensure_type(type).first);
     expr is_hset     = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
diff --git a/src/library/class_instance_synth.h b/src/library/class_instance_synth.h
index 8611840c9..e1c55d5ba 100644
--- a/src/library/class_instance_synth.h
+++ b/src/library/class_instance_synth.h
@@ -41,6 +41,8 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
                                  name const & prefix, expr const & type, bool use_local_instances = true,
                                  unifier_config const & cfg = unifier_config());
 
+optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
+
 /** \brief Try to synthesize an inhabitant for (is_hset type) using class instance resolution */
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);