diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 606e75711..140ede3fb 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -81,7 +81,8 @@ environment check_cmd(parser & p) {
     e = p.lambda_abstract(section_ps, e);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     e = p.elaborate(e, false);
-    expr type = type_checker(p.env()).check(e, ls);
+    type_checker tc(p.env(), p.mk_ngen(),  mk_default_converter(p.env(), true));
+    expr type = tc.check(e, ls);
     p.regular_stream() << e << " : " << type << endl;
     return p.env();
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 19b991ca0..4cb7af499 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -147,6 +147,7 @@ public:
     template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
 
     name mk_fresh_name() { return m_ngen.next(); }
+    name_generator mk_ngen() { return m_ngen.mk_child(); }
 
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }