diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index e1f16e9911..01412358e1 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -209,10 +209,11 @@ type_context::~type_context() { name type_context::get_local_pp_name(expr const & e) const { lean_assert(is_local(e)); - if (is_local_decl_ref(e)) - return m_lctx.get_local_decl(e)->get_pp_name(); - else - return local_pp_name(e); + if (is_local_decl_ref(e)) { + if (auto d = m_lctx.get_local_decl(e)) + return d->get_pp_name(); + } + return local_pp_name(e); } expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {