diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 12dcc3a932..e4372abe99 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2058,6 +2058,8 @@ public:
     lazy_type_context(environment const & env, options const & opts):m_env(env), m_opts(opts) {}
     virtual ~lazy_type_context() {}
     virtual environment const & env() const override { return const_cast<lazy_type_context*>(this)->ctx().env(); }
+    virtual local_context const & lctx() const override { return const_cast<lazy_type_context*>(this)->ctx().lctx(); }
+    virtual metavar_context const & mctx() const override { return const_cast<lazy_type_context*>(this)->ctx().mctx(); }
     virtual expr whnf(expr const & e) override { return ctx().whnf(e); }
     virtual bool is_def_eq(expr const & e1, expr const & e2) override { return ctx().is_def_eq(e1, e2); }
     virtual expr infer(expr const & e) override { return ctx().infer(e); }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 02f0fcc68f..50a9ba7fc7 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -17,8 +17,7 @@ formatter_factory mk_pretty_formatter_factory() {
     return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
         return formatter(o, [&](expr const & e, options const & new_o) {
             // what could ever go wrong
-            type_context_old & tctx = dynamic_cast<type_context_old &>(ctx);
-            return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), tctx.mctx().to_obj_arg(), tctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
+            return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), ctx.mctx().to_obj_arg(), ctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
         });
     };
 }
diff --git a/src/library/abstract_type_context.h b/src/library/abstract_type_context.h
index eb6ded4cc4..99a8e1bb7c 100644
--- a/src/library/abstract_type_context.h
+++ b/src/library/abstract_type_context.h
@@ -6,12 +6,16 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
+#include "library/local_context.h"
+#include "library/metavar_context.h"
 
 namespace lean {
 class abstract_type_context {
 public:
     virtual ~abstract_type_context() {}
     virtual environment const & env() const = 0;
+    virtual local_context const & lctx() const = 0;
+    virtual metavar_context const & mctx() const = 0;
     virtual expr whnf(expr const & e) = 0;
     virtual name next_name() = 0;
     virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 978e43c045..47d037124b 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -575,8 +575,8 @@ public:
     }
 
 
-    local_context const & lctx() const { return m_lctx; }
-    metavar_context const & mctx() const { return m_mctx; }
+    virtual local_context const & lctx() const override { return m_lctx; }
+    virtual metavar_context const & mctx() const override { return m_mctx; }
     expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
     expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
     optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }
diff --git a/stage0/src/frontends/lean/parser.cpp b/stage0/src/frontends/lean/parser.cpp
index 12dcc3a932..e4372abe99 100644
--- a/stage0/src/frontends/lean/parser.cpp
+++ b/stage0/src/frontends/lean/parser.cpp
@@ -2058,6 +2058,8 @@ public:
     lazy_type_context(environment const & env, options const & opts):m_env(env), m_opts(opts) {}
     virtual ~lazy_type_context() {}
     virtual environment const & env() const override { return const_cast<lazy_type_context*>(this)->ctx().env(); }
+    virtual local_context const & lctx() const override { return const_cast<lazy_type_context*>(this)->ctx().lctx(); }
+    virtual metavar_context const & mctx() const override { return const_cast<lazy_type_context*>(this)->ctx().mctx(); }
     virtual expr whnf(expr const & e) override { return ctx().whnf(e); }
     virtual bool is_def_eq(expr const & e1, expr const & e2) override { return ctx().is_def_eq(e1, e2); }
     virtual expr infer(expr const & e) override { return ctx().infer(e); }
diff --git a/stage0/src/frontends/lean/pp.cpp b/stage0/src/frontends/lean/pp.cpp
index 02f0fcc68f..50a9ba7fc7 100644
--- a/stage0/src/frontends/lean/pp.cpp
+++ b/stage0/src/frontends/lean/pp.cpp
@@ -17,8 +17,7 @@ formatter_factory mk_pretty_formatter_factory() {
     return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
         return formatter(o, [&](expr const & e, options const & new_o) {
             // what could ever go wrong
-            type_context_old & tctx = dynamic_cast<type_context_old &>(ctx);
-            return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), tctx.mctx().to_obj_arg(), tctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
+            return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), ctx.mctx().to_obj_arg(), ctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
         });
     };
 }
diff --git a/stage0/src/library/abstract_type_context.h b/stage0/src/library/abstract_type_context.h
index eb6ded4cc4..99a8e1bb7c 100644
--- a/stage0/src/library/abstract_type_context.h
+++ b/stage0/src/library/abstract_type_context.h
@@ -6,12 +6,16 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
+#include "library/local_context.h"
+#include "library/metavar_context.h"
 
 namespace lean {
 class abstract_type_context {
 public:
     virtual ~abstract_type_context() {}
     virtual environment const & env() const = 0;
+    virtual local_context const & lctx() const = 0;
+    virtual metavar_context const & mctx() const = 0;
     virtual expr whnf(expr const & e) = 0;
     virtual name next_name() = 0;
     virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
diff --git a/stage0/src/library/type_context.h b/stage0/src/library/type_context.h
index 978e43c045..47d037124b 100644
--- a/stage0/src/library/type_context.h
+++ b/stage0/src/library/type_context.h
@@ -575,8 +575,8 @@ public:
     }
 
 
-    local_context const & lctx() const { return m_lctx; }
-    metavar_context const & mctx() const { return m_mctx; }
+    virtual local_context const & lctx() const override { return m_lctx; }
+    virtual metavar_context const & mctx() const override { return m_mctx; }
     expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
     expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
     optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }