diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 062f86c267..ef3a29b59e 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1914,14 +1914,4 @@ static options mk_options(bool detail) {
     }
     return opts;
 }
-
-static void pp_core(environment const & env, expr const & e, bool detail) {
-    old_type_checker tc(env);
-    io_state ios(mk_pretty_formatter_factory(), mk_options(detail));
-    regular(env, ios, tc) << e << "\n";
 }
-
-}
-// for debugging purposes
-void pp(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, false); }
-void pp_detail(lean::environment const & env, lean::expr const & e) { lean::pp_core(env, e, true); }
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index 449108a315..c443b8c19a 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/quot.h"
-#include "kernel/old_type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/trace.h"
 #include "library/sorry.h"
@@ -323,7 +322,6 @@ static void print_recursor_info(parser & p, message_builder & out) {
 }
 
 static bool print_constant(parser const & p, message_builder & out, char const * kind, declaration const & d, bool is_def = false) {
-    old_type_checker tc(p.env());
     print_attributes(p, out, d.get_name());
     if (is_protected(p.env(), d.get_name()))
         out << "protected ";
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index b410e61fe1..228040694b 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
-#include "kernel/old_type_checker.h"
+#include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/error_msgs.h"
 #include "library/replace_visitor.h"