diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp
index eeec579ffc..18f654bb9a 100644
--- a/src/library/inductive_compiler/mutual.cpp
+++ b/src/library/inductive_compiler/mutual.cpp
@@ -231,7 +231,7 @@ class add_mutual_inductive_decl_fn {
     }
 
     expr translate_ir(unsigned ind_idx, expr const & ir) {
-        name ir_name = mlocal_name(m_mut_decl.get_ind(ind_idx)) + mlocal_name(ir).replace_prefix(m_basic_prefix, name());
+        name ir_name = m_basic_ind_name + name(mlocal_name(ir).get_string()).append_after(ind_idx);
         buffer<expr> locals;
         expr ty = m_tctx.whnf(mlocal_type(ir));
         while (is_pi(ty)) {
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index e35ed3b9bb..ee4ed1570d 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -197,6 +197,10 @@ class add_nested_inductive_decl_fn {
     name mk_inner_name(name const & n) {
         if (m_nested_decl.is_ind_name(n) || m_nested_decl.is_ir_name(n)) {
             return nest(n);
+        } else if (!n.is_atomic()) {
+            // We want the atomic introduction rule name to stay at the end, but we don't want to introduce
+            // a new "nest_" in the beginning.
+            return nest(n.get_prefix() + mlocal_name(m_nested_decl.get_ind(0)) + name(n.get_string()));
         } else {
             // We append the ind name at the end so that we don't put the "nest_" in the beginning
             return nest(n + mlocal_name(m_nested_decl.get_ind(0)));