diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 813bad3814..373634ba72 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -39,14 +39,17 @@ name pretty_fn::mk_metavar_name(name const & m) {
     return new_m;
 }
 
-name pretty_fn::mk_local_name(name const & m) {
+name pretty_fn::mk_local_name(name const & n, name const & suggested) {
+    if (auto it = m_purify_local_table.find(n))
+        return *it;
     unsigned i = 1;
-    name r = m;
-    while (m_purify_locals.contains(r)) {
-        r = m.append_after(i);
+    name r = suggested;
+    while (m_purify_used_locals.contains(r)) {
+        r = suggested.append_after(i);
         i++;
     }
-    m_purify_locals.insert(r);
+    m_purify_used_locals.insert(r);
+    m_purify_local_table.insert(n, r);
     return r;
 }
 
@@ -77,7 +80,7 @@ expr pretty_fn::purify(expr const & e) {
             else if (is_metavar(e))
                 return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e)));
             else if (is_local(e))
-                return some_expr(mk_local(mlocal_name(e), mk_local_name(local_pp_name(e)), mlocal_type(e), local_info(e)));
+                return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e)));
             else if (is_constant(e))
                 return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); })));
             else if (is_sort(e))
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 47a9a71851..6afa78303f 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -26,7 +26,8 @@ private:
     name               m_meta_prefix;
     unsigned           m_next_meta_idx;
     name_map<name>     m_purify_meta_table;
-    name_set           m_purify_locals;
+    name_map<name>     m_purify_local_table;
+    name_set           m_purify_used_locals;
     // cached configuration
     unsigned           m_indent;
     unsigned           m_max_depth;
@@ -41,7 +42,7 @@ private:
 
     unsigned max_bp() const { return std::numeric_limits<unsigned>::max(); }
     name mk_metavar_name(name const & m);
-    name mk_local_name(name const & m);
+    name mk_local_name(name const & n, name const & suggested);
     level purify(level const & l);
     expr purify(expr const & e);
     result mk_result(format const & e, unsigned rbp) const { return mk_pair(e, rbp); }
diff --git a/tests/lean/t4.lean.expected.out b/tests/lean/t4.lean.expected.out
index e93f5b4959..3fc13ad66a 100644
--- a/tests/lean/t4.lean.expected.out
+++ b/tests/lean/t4.lean.expected.out
@@ -5,8 +5,8 @@ F : Type → Type
 F : Type → Type
 f : N → N → N
 len : Π (A : Type) (n : N), vec A n → N
-B → B_1 : Bool
-A → A_1 : Type
+B → B : Bool
+A → A : Type
 C : Type
 t4.lean:25:6: error: unknown identifier 'A'
 R : Type → Bool