diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4beb767275..c75fa01b5f 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -597,7 +597,7 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
     auto short_n = n;
     if (!m_full_names) {
         if (auto it = is_aliased(n)) {
-            if (!m_private_names || !hidden_to_user_name(m_env, n))
+            if (!m_private_names || !private_to_user_name(m_env, n))
                 short_n = *it;
         } else {
             for (name const & ns : get_namespaces(m_env)) {
@@ -614,7 +614,7 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
         }
     }
     if (!m_private_names) {
-        if (auto n1 = hidden_to_user_name(m_env, short_n))
+        if (auto n1 = private_to_user_name(m_env, short_n))
             short_n = *n1;
     }
     if (m_ctx.is_local_user_name(short_n.get_root())) {
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index aaffaf0db0..008b607b7d 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -207,7 +207,7 @@ static void print_patterns(parser & p, name const & n) {
 #endif
 
 static name to_user_name(environment const & env, name const & n) {
-    if (auto r = hidden_to_user_name(env, n))
+    if (auto r = private_to_user_name(env, n))
         return *r;
     else
         return n;
diff --git a/src/library/private.cpp b/src/library/private.cpp
index 193e421bd0..9e0e3a4f07 100644
--- a/src/library/private.cpp
+++ b/src/library/private.cpp
@@ -128,13 +128,13 @@ environment register_private_name(environment const & env, name const & n, name
     return preserve_private_data(new_env, prv_n, n);
 }
 
-optional<name> hidden_to_user_name(environment const & env, name const & n) {
+optional<name> private_to_user_name(environment const & env, name const & n) {
     auto it = get_extension(env).m_inv_map.find(n);
     return it ? optional<name>(*it) : optional<name>();
 }
 
 bool is_private(environment const & env, name const & n) {
-    return static_cast<bool>(hidden_to_user_name(env, n));
+    return static_cast<bool>(private_to_user_name(env, n));
 }
 
 void initialize_private() {
diff --git a/src/library/private.h b/src/library/private.h
index e13133f207..5d2d280002 100644
--- a/src/library/private.h
+++ b/src/library/private.h
@@ -16,21 +16,20 @@ namespace lean {
 pair<environment, name> add_private_name(environment const & env, name const & n);
 
 /**
-    \brief Return the user name associated with the hidden name \c n.
+    \brief Return the user name associated with the private name \c n.
 
-    \remark The "user name" is the argument provided to \c add_private_name, and "hidden name" is the name returned
+    \remark The "user name" is the argument provided to \c add_private_name, and "private name" is the name returned
     by \c add_private_name.
 */
-optional<name> hidden_to_user_name(environment const & env, name const & n);
+optional<name> private_to_user_name(environment const & env, name const & n);
 
 bool is_private(environment const & env, name const & n);
 
 /* Create a private prefix that is going to be use to generate many private names.
    This function registers the private prefix in the environment. */
 pair<environment, name> mk_private_prefix(environment const & env);
-pair<environment, name> mk_private_prefix(environment const & env, name const & n);
 
-/* Create a private name based on \c c and get_pos_info_provider(), and register it using \c add_private_name */
+/* Create a private name based on \c c, and register it using \c add_private_name */
 pair<environment, name> mk_private_name(environment const & env, name const & c);
 
 /* Register a \c n as the name for private name \c prv_n. \c prv_n must have been constructed using