diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index e4ad75c75..d6cb9bacb 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -48,20 +48,10 @@ environment add_alias(environment const & env, name const & a, expr const & e, i
     return update(env, ext);
 }
 
-environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios) {
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios) {
     return add_aliases(env, prefix, new_prefix, 0, nullptr, ios);
 }
 
-static name replace_prefix(name const & n, name const & prefix, optional<name> const & new_prefix) {
-    if (n == prefix)
-        return new_prefix ? *new_prefix : name();
-    name p = replace_prefix(n.get_prefix(), prefix, new_prefix);
-    if (n.is_string())
-        return name(p, n.get_string());
-    else
-        return name(p, n.get_numeral());
-}
-
 static optional<expr> get_fix_param(unsigned num_fix_params, std::pair<name, expr> const * fix_params, name const & n) {
     for (unsigned i = 0; i < num_fix_params; i++) {
         if (fix_params[i].first == n)
@@ -72,12 +62,12 @@ static optional<expr> get_fix_param(unsigned num_fix_params, std::pair<name, exp
 
 static name g_local_name = name::mk_internal_unique_name();
 
-environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix,
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
                         unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios) {
     aliases_ext ext = get_extension(env);
     env.for_each([&](declaration const & d) {
             if (is_prefix_of(prefix, d.get_name())) {
-                name a        = replace_prefix(d.get_name(), prefix, new_prefix);
+                name a        = d.get_name().replace_prefix(prefix, new_prefix);
                 check_name(env, a, ios);
                 levels ls     = map2<level>(d.get_params(), [](name const &) { return mk_level_placeholder(); });
                 expr c        = mk_constant(d.get_name(), ls);
@@ -144,11 +134,11 @@ static int add_alias(lua_State * L) {
 static int add_aliases(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2) {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), optional<name>(), get_io_state(L)));
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), name(), get_io_state(L)));
     } else if (nargs == 3) {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_optional_name(L, 3), get_io_state(L)));
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), get_io_state(L)));
     } else if (nargs == 4 && is_io_state(L, 4)) {
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_optional_name(L, 3), to_io_state(L, 4)));
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
     } else {
         buffer<std::pair<name, expr>> fix_params;
         luaL_checktype(L, 4, LUA_TTABLE);
@@ -164,7 +154,7 @@ static int add_aliases(lua_State * L) {
             lua_pop(L, 2);
             fix_params.emplace_back(n, e);
         }
-        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_optional_name(L, 3),
+        return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3),
                                                fix_params.size(), fix_params.data(), to_io_state_ext(L, 5)));
     }
 }
diff --git a/src/library/aliases.h b/src/library/aliases.h
index 9f923e17e..53713d1de 100644
--- a/src/library/aliases.h
+++ b/src/library/aliases.h
@@ -18,18 +18,20 @@ namespace lean {
 */
 environment add_alias(environment const & env, name const & a, expr const & e, io_state const & ios);
 /**
-   \brief Create an alias for each declaration named <tt>prefix.rest</tt>. If \c new_prefix is not none,
-   then the alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>. Otherwise, it is just \c rest.
+   \brief Create an alias for each declaration named <tt>prefix.rest</tt>.
+   The alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>.
    Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
+
+   \remark \c new_prefix may be the anonymous name.
 */
-environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios);
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios);
 /**
    \brief Create an alias for each declaration named <tt>prefix.rest</tt>, the alias will also fix the value of parameters
    in \c fix_params. The argument \c fix_params is a sequence of pairs <tt>(name, expr)</tt>, where the \c name is the
    name of the parameter to be fixed.
    Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
 */
-environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix,
+environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
                         unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios);
 
 /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 8479beab9..1f6d96c9c 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -387,6 +387,18 @@ name name::append_after(unsigned i) const {
     return append_after(s.str().c_str());
 }
 
+name name::replace_prefix(name const & prefix, name const & new_prefix) const {
+    if (*this == prefix)
+        return new_prefix;
+    if (is_anonymous())
+        return *this;
+    name p = get_prefix().replace_prefix(prefix, new_prefix);
+    if (is_string())
+        return name(p, get_string());
+    else
+        return name(p, get_numeral());
+}
+
 enum name_ll_kind { LL_ANON = 0, LL_STRING = 1, LL_INT = 2, LL_STRING_PREFIX = 3, LL_INT_PREFIX = 4 };
 name_ll_kind ll_kind(name const & n) {
     if (n.is_anonymous())
@@ -478,6 +490,8 @@ static int mk_name(lua_State * L) {
 name to_name_ext(lua_State * L, int idx) {
     if (lua_isstring(L, idx)) {
         return luaL_checkstring(L, idx);
+    } else if (lua_isnil(L, idx)) {
+        return name();
     } else if (lua_istable(L, idx)) {
         name r;
         int n = objlen(L, idx);
@@ -548,21 +562,24 @@ static int name_append_after(lua_State * L) {
         return push_name(L, to_name(L, 1).append_after(lua_tostring(L, 2)));
 }
 
+static int name_replace_prefix(lua_State * L) { return push_name(L, to_name(L, 1).replace_prefix(to_name_ext(L, 2), to_name_ext(L, 3))); }
+
 static const struct luaL_Reg name_m[] = {
-    {"__gc",          name_gc}, // never throws
-    {"__tostring",    safe_function<name_tostring>},
-    {"__eq",          safe_function<name_eq>},
-    {"__lt",          safe_function<name_lt>},
-    {"is_atomic",     safe_function<name_is_atomic>},
-    {"is_anonymous",  safe_function<name_is_anonymous>},
-    {"is_numeral",    safe_function<name_is_numeral>},
-    {"is_string",     safe_function<name_is_string>},
-    {"get_prefix",    safe_function<name_get_prefix>},
-    {"get_numeral",   safe_function<name_get_numeral>},
-    {"get_string",    safe_function<name_get_string>},
-    {"hash",          safe_function<name_hash>},
-    {"append_before", safe_function<name_append_before>},
-    {"append_after",  safe_function<name_append_after>},
+    {"__gc",           name_gc}, // never throws
+    {"__tostring",     safe_function<name_tostring>},
+    {"__eq",           safe_function<name_eq>},
+    {"__lt",           safe_function<name_lt>},
+    {"is_atomic",      safe_function<name_is_atomic>},
+    {"is_anonymous",   safe_function<name_is_anonymous>},
+    {"is_numeral",     safe_function<name_is_numeral>},
+    {"is_string",      safe_function<name_is_string>},
+    {"get_prefix",     safe_function<name_get_prefix>},
+    {"get_numeral",    safe_function<name_get_numeral>},
+    {"get_string",     safe_function<name_get_string>},
+    {"hash",           safe_function<name_hash>},
+    {"append_before",  safe_function<name_append_before>},
+    {"append_after",   safe_function<name_append_after>},
+    {"replace_prefix", safe_function<name_replace_prefix>},
     {0, 0}
 };
 
diff --git a/src/util/name.h b/src/util/name.h
index 1e716edf8..bf91fdcf0 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -121,6 +121,12 @@ public:
     */
     name append_after(unsigned i) const;
 
+    /**
+        \brief If prefix is a prefix of this name, then return a new name where the prefix is replaced with new_prefix.
+        Otherwise, return this name.
+    */
+    name replace_prefix(name const & prefix, name const & new_prefix) const;
+
     friend void swap(name & a, name & b) {
         std::swap(a.m_ptr, b.m_ptr);
     }
diff --git a/tests/lua/n7.lua b/tests/lua/n7.lua
new file mode 100644
index 000000000..54a9cb4f0
--- /dev/null
+++ b/tests/lua/n7.lua
@@ -0,0 +1,7 @@
+local n1 = name("foo", "bar", 1)
+assert(n1:replace_prefix("foo", {"hello", "world"}) == name("hello", "world", "bar", 1))
+assert(n1:replace_prefix("foo2", {"hello", "world"}) == name("foo", "bar", 1))
+assert(n1:replace_prefix("foo", nil) == name("bar", 1))
+assert(n1:replace_prefix("foo", name()) == name("bar", 1))
+assert(n1:replace_prefix({"foo", "bar"}, {"hello", "world"}) == name("hello", "world", 1))
+assert(n1:replace_prefix({"foo", "bar"}, "tst") == name("tst", 1))