diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 675ac3b37b..730b7e35d2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -63,6 +63,10 @@ elaborator::elaborator(environment const & env, options const & opts, metavar_co
     m_ctx(mctx, lctx, get_elab_tc_cache_for(env, opts), transparency_mode::Semireducible) {
 }
 
+auto elaborator::mk_pp_ctx(type_context const & ctx) -> pp_fn {
+    return ::lean::mk_pp_ctx(ctx.env(), m_opts, ctx.mctx(), ctx.lctx());
+}
+
 format elaborator::pp_indent(pp_fn const & pp_fn, expr const & e) {
     unsigned i = get_pp_indent(m_opts);
     return nest(i, line() + pp_fn(e));
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 67e5350001..8ee268262a 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -83,6 +83,7 @@ private:
     expr get_default_numeral_type();
 
     typedef std::function<format(expr const &)> pp_fn;
+    pp_fn mk_pp_ctx(type_context const & ctx);
     format pp_indent(pp_fn const & pp_fn, expr const & e);
     format pp_indent(expr const & e);
     format pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns);