diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 6750d8aea..f010918c2 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -184,7 +184,7 @@ auto pretty_fn::pp_const(expr const & e) -> result {
             for (name const & ns : get_namespaces(m_env)) {
                 if (!ns.is_anonymous()) {
                     name new_n = n.replace_prefix(ns, name());
-                    if (new_n != n) {
+                    if (new_n != n && !new_n.is_anonymous()) {
                         n = new_n;
                         break;
                     }
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 23bd7822d..dd7eaa739 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -188,7 +188,8 @@ environment add_aliases(environment const & env, name const & prefix, name const
     env.for_each_declaration([&](declaration const & d) {
             if (is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
                 name a        = d.get_name().replace_prefix(prefix, new_prefix);
-                ext.add_expr_alias(a, d.get_name());
+                if (!a.is_anonymous())
+                    ext.add_expr_alias(a, d.get_name());
             }
         });
     env.for_each_universe([&](name const & u) {
@@ -196,7 +197,8 @@ environment add_aliases(environment const & env, name const & prefix, name const
                 name a = u.replace_prefix(prefix, new_prefix);
                 if (env.is_universe(a))
                     throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
-                ext.add_level_alias(a, u);
+                if (!a.is_anonymous())
+                    ext.add_level_alias(a, u);
             }
         });
     return update(env, ext);