diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 3fafe93e42..796a854519 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2344,7 +2344,7 @@ public:
     virtual expr infer(expr const & e) override { return ctx().infer(e); }
     virtual expr check(expr const & e) override { return ctx().check(e); }
     virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
-    virtual name mk_fresh_name() override { return ctx().mk_fresh_name(); }
+    virtual name next_name() override { return ctx().next_name(); }
 };
 
 void parser::parse_command(cmd_meta const & meta) {
diff --git a/src/kernel/abstract_type_context.cpp b/src/kernel/abstract_type_context.cpp
index d60c67cffc..0d3078afa8 100644
--- a/src/kernel/abstract_type_context.cpp
+++ b/src/kernel/abstract_type_context.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
-    return mk_local(mk_fresh_name(), pp_name, type, bi);
+    return mk_local(next_name(), pp_name, type, bi);
 }
 
 void abstract_type_context::pop_local() {
diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h
index 43f43a33ff..fb56f9f674 100644
--- a/src/kernel/abstract_type_context.h
+++ b/src/kernel/abstract_type_context.h
@@ -20,7 +20,7 @@ public:
     virtual ~abstract_type_context() {}
     virtual environment const & env() const = 0;
     virtual expr whnf(expr const & e) = 0;
-    virtual name mk_fresh_name() = 0;
+    virtual name next_name() = 0;
     virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
     virtual bool is_def_eq(expr const & e1, expr const & e2) = 0;
     virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) { return is_def_eq(e1, e2); }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index d0ce599b9e..e5fa53f584 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -85,7 +85,7 @@ public:
 
     virtual environment const & env() const { return m_env; }
 
-    virtual name mk_fresh_name() { return m_name_generator.next(); }
+    virtual name next_name() { return m_name_generator.next(); }
 
     /** \brief Return the type of \c t.
         It does not check whether the input expression is type correct or not.
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 25f07c47d5..152795f287 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -714,7 +714,7 @@ public:
     virtual environment const & env() const override { return m_cache->m_env; }
 
     // TODO(Leo): avoid ::lean::mk_fresh_name
-    virtual name mk_fresh_name() override { return ::lean::mk_fresh_name(); }
+    virtual name next_name() override { return ::lean::mk_fresh_name(); }
 
     options const & get_options() const { return m_cache->m_options; }
     local_context const & lctx() const { return m_lctx; }
@@ -1171,7 +1171,7 @@ public:
     virtual expr infer(expr const & e) override;
     virtual expr whnf(expr const & e) override;
     virtual bool is_def_eq(expr const & e1, expr const & e2) override;
-    virtual name mk_fresh_name() override { return m_ctx.mk_fresh_name(); }
+    virtual name next_name() override { return m_ctx.next_name(); }
 
     bool match(expr const & e1, expr const & e2);