diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp
index baa9736837..0121ef0ab6 100644
--- a/src/library/aux_definition.cpp
+++ b/src/library/aux_definition.cpp
@@ -59,7 +59,7 @@ levels closure_helper::collect(levels const & ls) {
         return levels(r);
 }
 
-expr closure_helper::collect(expr const & e) {
+expr closure_helper::collect(expr const & e, name_set const & except_locals) {
     lean_assert(!m_finalized_collection);
     return replace(e, [&](expr const & e, unsigned) {
             if (is_metavar(e)) {
@@ -76,7 +76,7 @@ expr closure_helper::collect(expr const & e) {
                 }
             } else if (is_local(e)) {
                 name const & id = mlocal_name(e);
-                if (!m_found_local.contains(id)) {
+                if (!m_found_local.contains(id) && !except_locals.contains(id)) {
                     m_found_local.insert(id);
                     m_params.push_back(e);
                 }
diff --git a/src/library/aux_definition.h b/src/library/aux_definition.h
index 140ab2e1e0..7852a23724 100644
--- a/src/library/aux_definition.h
+++ b/src/library/aux_definition.h
@@ -54,8 +54,11 @@ public:
     level collect(level const & l);
     /* \pre finalize_collection has not been invoked */
     levels collect(levels const & ls);
-    /* \pre finalize_collection has not been invoked */
-    expr collect(expr const & e);
+    /*
+       \remark Locals at `except_locals` are not collected.
+       \pre finalize_collection has not been invoked */
+    expr collect(expr const & e, name_set const & except_locals);
+    expr collect(expr const & e) { return collect(e, name_set()); }
 
     /* \pre finalize_collection has not been invoked */
     void finalize_collection();
diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp
index 95179aec61..dbba0f6930 100644
--- a/src/library/compiler/elim_recursors.cpp
+++ b/src/library/compiler/elim_recursors.cpp
@@ -18,7 +18,6 @@ Author: Leonardo de Moura
 #include "library/compiler/procedure.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/compiler_step_visitor.h"
-#include "library/compiler/rec_fn_macro.h"
 
 namespace lean {
 class elim_recursors_fn : public compiler_step_visitor {
@@ -114,7 +113,7 @@ protected:
         /* Create expr (rec_fn) for representing recursive calls. */
         expr aux_decl_type = ctx().infer(aux);
         name aux_decl_name = mk_compiler_unused_name(m_env, m_prefix, "_rec", m_idx);
-        expr rec_fn = mk_rec_fn_macro(aux_decl_name, aux_decl_type);
+        expr rec_fn = mk_constant(aux_decl_name, const_levels(fn));
         /* Create new locals for aux.
            The operating abstract_locals creates a lambda-abstraction around aux if it uses
            local constants. */
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index f27796a97b..708f736bd4 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/compiler/util.h"
 #include "library/compiler/nat_value.h"
 #include "library/compiler/comp_irrelevant.h"
-#include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/compiler_step_visitor.h"
 
 namespace lean {
@@ -65,8 +64,6 @@ class erase_irrelevant_fn : public compiler_step_visitor {
             return *g_neutral_expr;
         } else if (is_comp_irrelevant(e)) {
             return *g_neutral_expr;
-        } else if (is_rec_fn_macro(e)) {
-            return mk_constant(get_rec_fn_name(e));
         } else if (is_nat_value(e)) {
             return e;
         } else if (auto r = macro_def(e).expand(e, m_ctx)) {
diff --git a/src/library/compiler/erase_irrelevant.h b/src/library/compiler/erase_irrelevant.h
index ab40a8e006..0cf2980b9d 100644
--- a/src/library/compiler/erase_irrelevant.h
+++ b/src/library/compiler/erase_irrelevant.h
@@ -12,11 +12,7 @@ class abstract_context_cache;
     The parameters, motive and indices are also erased from cases_on applications.
 
     \remark The resultant term cannot be type checked. So, any preprocessing step
-    that requires type inference cannot be applied after this transformation.
-
-    \remark This procedure also replace occurrences of rec_fn_macro with constants.
-    The rec_fn_macro is only used to make sure the result type checks.
-    So, since the result will not type check anyway, there is no point in using them. */
+    that requires type inference cannot be applied after this transformation.  */
 expr erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e);
 /** \brief Neutral auxiliary term. */
 bool is_neutral_expr(expr const & e);
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 6a3826fd1e..46f5c22ad8 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -39,6 +39,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 class expand_aux_fn : public compiler_step_visitor {
+    name_set m_decl_names; /* functions being compiled */
+
     enum class recursor_kind { Aux, CasesOn, NotRecursor };
     /* We only expand auxiliary recursors and user-defined recursors.
        However, we don't unfold recursors of the form C.cases_on if C != eq. */
@@ -98,10 +100,16 @@ class expand_aux_fn : public compiler_step_visitor {
         return is_constant(e) && ::lean::is_inline(env(), const_name(e));
     }
 
+    bool is_function_being_compiled(expr const & e) const {
+        expr const & f = get_app_fn(e);
+        return is_constant(f) && m_decl_names.contains(const_name(f));
+    }
+
     bool should_unfold(expr const & e) {
         return
-            (is_not_vm_function(e) && !ctx().is_proof(e) && !is_pack_unpack(e) && !is_noncomputable_const(e)) ||
-            (is_inline(e));
+            !is_function_being_compiled(e) &&
+            ((is_not_vm_function(e) && !ctx().is_proof(e) && !is_pack_unpack(e) && !is_noncomputable_const(e)) ||
+             (is_inline(e)));
     }
 
     expr unfold(expr const & e) {
@@ -150,11 +158,13 @@ class expand_aux_fn : public compiler_step_visitor {
     }
 
 public:
-    expand_aux_fn(environment const & env, abstract_context_cache & cache):compiler_step_visitor(env, cache) {}
+    expand_aux_fn(environment const & env, name_set const & decl_names, abstract_context_cache & cache):
+        compiler_step_visitor(env, cache),
+        m_decl_names(decl_names) {}
 };
 
-static expr expand_aux(environment const & env, abstract_context_cache & cache, expr const & e) {
-    return expand_aux_fn(env, cache)(e);
+static expr expand_aux(environment const & env, name_set const & ns, abstract_context_cache & cache, expr const & e) {
+    return expand_aux_fn(env, ns, cache)(e);
 }
 
 static name * g_tmp_prefix = nullptr;
@@ -162,6 +172,7 @@ static name * g_tmp_prefix = nullptr;
 class preprocess_fn {
     environment    m_env;
     context_cache  m_cache;
+    name_set       m_decl_names; /* name of the functions being compiled */
 
     bool check(declaration const & d, expr const & v) {
         bool memoize       = true;
@@ -185,25 +196,6 @@ class preprocess_fn {
         }
     }
 
-#if 0
-    void dump_pos_info(expr const & v) {
-        std::cout << v << "\n\n";
-        for_each(v, [&](expr const & e, unsigned) {
-                auto pip = get_pos_info_provider();
-                if (!pip) return false;
-                if (auto p = pip->get_pos_info(e))
-                    std::cout << "pos[" << ((unsigned)e.kind()) << "]: " << p->first << ":" << p->second << "\n"
-                              << e << "\n";
-                return true;
-            });
-        std::cout << "------------\n";
-    }
-
-    void dump_pos_info(buffer<pair<name, expr>> & procs) {
-        for (auto p : procs) dump_pos_info(p.second);
-    }
-#endif
-
     /* If type of d is a proposition or return a type, we don't need to compile it.
        We can just generate (fun args, neutral_expr)
 
@@ -230,8 +222,16 @@ class preprocess_fn {
     }
 
 public:
-    preprocess_fn(environment const & env):
-        m_env(env) {}
+    preprocess_fn(environment const & env, declaration const & d):
+        m_env(env) {
+        m_decl_names.insert(d.get_name());
+    }
+
+    preprocess_fn(environment const & env, buffer<declaration> const & ds):
+        m_env(env) {
+        for (declaration const & d : ds)
+            m_decl_names.insert(d.get_name());
+    }
 
     void operator()(declaration const & d, buffer<procedure> & procs) {
         if (compile_irrelevant(d, procs))
@@ -241,7 +241,7 @@ public:
         v = inline_simple_definitions(m_env, m_cache, v);
         lean_cond_assert("compiler", check(d, v));
         lean_trace(name({"compiler", "inline"}), tout() << "\n" << v << "\n";);
-        v = expand_aux(m_env, m_cache, v);
+        v = expand_aux(m_env, m_decl_names, m_cache, v);
         lean_cond_assert("compiler", check(d, v));
         lean_trace(name({"compiler", "expand_aux"}), tout() << "\n" << v << "\n";);
         v = mark_comp_irrelevant_subterms(m_env, m_cache, v);
@@ -276,13 +276,14 @@ public:
 };
 
 void preprocess(environment const & env, declaration const & d, buffer<procedure> & result) {
-    return preprocess_fn(env)(d, result);
+    return preprocess_fn(env, d)(d, result);
 }
 
 void preprocess(environment const & env, buffer<declaration> const & ds, buffer<procedure> & result) {
+    preprocess_fn F(env, ds);
     for (declaration const & d : ds) {
         buffer<procedure> procs;
-        preprocess(env, d, procs);
+        F(d, procs);
         result.append(procs);
     }
 }
diff --git a/src/library/compiler/reduce_arity.cpp b/src/library/compiler/reduce_arity.cpp
index 365b55ce22..bdf6d4cbe1 100644
--- a/src/library/compiler/reduce_arity.cpp
+++ b/src/library/compiler/reduce_arity.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/for_each_fn.h"
 #include "library/trace.h"
-#include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/procedure.h"
 #include "library/compiler/compiler_step_visitor.h"
 
@@ -30,13 +29,6 @@ class remove_args_fn : public compiler_step_visitor {
     /* Mapping from auxiliary function name to bitvector of used arguments */
     name_map<std::vector<bool>> const & m_to_reduce;
 
-    virtual expr visit_macro(expr const & e) override {
-        /* This module assumes rec_fn_macros have already been eliminated.
-           Remark: the step erase_irrelevant eliminates all occurences. */
-        lean_assert(!is_rec_fn_macro(e));
-        return compiler_step_visitor::visit_macro(e);
-    }
-
     virtual expr visit_app(expr const & e) override {
         expr const & fn = get_app_fn(e);
         if (is_constant(fn)) {
diff --git a/src/library/compiler/reduce_arity.h b/src/library/compiler/reduce_arity.h
index 655761345b..e3cf315eba 100644
--- a/src/library/compiler/reduce_arity.h
+++ b/src/library/compiler/reduce_arity.h
@@ -13,9 +13,6 @@ namespace lean {
 /** \brief Try to reduce the arity of auxiliary declarations in procs.
     It assumes all but the last entry are auxiliary declarations.
 
-    \remark This procedure assumes rec_fn_macro has already been eliminated.
-    The procedure erase_irrelevant can be used to accomplish that.
-
     \remark This step does not rely on type information. That is,
     the input expressions don't need to be type checkable. */
 void reduce_arity(environment const & env, abstract_context_cache & cache, buffer<procedure> & procs);
diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h
index 9fac5dca77..a9c87c38ee 100644
--- a/src/library/equations_compiler/equations.h
+++ b/src/library/equations_compiler/equations.h
@@ -39,8 +39,8 @@ expr get_as_pattern_rhs(expr const & e);
 
 struct equations_header {
     unsigned   m_num_fns{0};              /* number of functions being defined */
-    names m_fn_names;                /* local names for functions */
-    names m_fn_actual_names;         /* Full qualified name and/or private name */
+    names      m_fn_names;                /* local names for functions */
+    names      m_fn_actual_names;         /* Full qualified name and/or private name */
     bool       m_is_private{false};       /* if true, it must be a private definition */
     bool       m_is_lemma{false};         /* if true, equations are defining a lemma */
     bool       m_is_meta{false};          /* the auxiliary declarations should be tagged as meta */
diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp
index f4d1e210d8..259cd8b0a1 100644
--- a/src/library/equations_compiler/unbounded_rec.cpp
+++ b/src/library/equations_compiler/unbounded_rec.cpp
@@ -22,38 +22,30 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 
 namespace lean {
-static expr replace_rec_apps(type_context_old & ctx, expr const & e) {
-    equations_header const & header = get_equations_header(e);
-    names actual_names = header.m_fn_actual_names;
-    unpack_eqns ues(ctx, e);
-    buffer<expr> fns;
-    buffer<expr> macro_fns;
-    for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
-        expr const & fn = ues.get_fn(fidx);
-        fns.push_back(fn);
-        macro_fns.push_back(mk_rec_fn_macro(head(actual_names), ctx.infer(fn)));
-        actual_names = tail(actual_names);
-    }
-    for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
-        buffer<expr> & eqns = ues.get_eqns_of(fidx);
-        for (expr & eqn : eqns) {
-            unpack_eqn ue(ctx, eqn);
-            expr new_rhs = replace_locals(ue.rhs(), fns, macro_fns);
-            ue.rhs() = new_rhs;
-            eqn = ue.repack();
-        }
-    }
-    expr r = ues.repack();
-    lean_trace("eqn_compiler", tout() << "using unbounded recursion (meta-definition):\n" << r << "\n";);
-    return r;
-}
 
-static void split_rec_fns(type_context_old & ctx, expr const & e, buffer<expr> & result) {
+static local_context split_rec_fns(environment const & env, metavar_context & mctx, local_context const & lctx, expr const & e, buffer<expr> & aux_rec_fns, buffer<expr> & result) {
     equations_header const & header = get_equations_header(e);
-    unpack_eqns ues(ctx, e);
+    type_context_old ctx1(env, options(), mctx, lctx, transparency_mode::Semireducible); // TODO(Leo): fix options
+    unpack_eqns ues1(ctx1, e);
+    /* Create declarations for recursive functions at `new_lctx` */
+    local_context new_lctx = lctx;
+    for (unsigned fidx = 0; fidx < ues1.get_num_fns(); fidx++) {
+        expr const & fn = ues1.get_fn(fidx);
+        expr aux_rec_fn = new_lctx.mk_local_decl(name(mlocal_pp_name(fn), "_rec"), ctx1.infer(fn), local_info(fn));
+        aux_rec_fns.push_back(aux_rec_fn);
+    }
+
+    /* Split equations, and replace recursive calls with aux_rec_fns */
+    type_context_old ctx2(env, options(), ctx1.mctx(), new_lctx, transparency_mode::Semireducible); // TODO(Leo): fix options
+    unpack_eqns ues2(ctx2, e);
     names fn_names        = header.m_fn_names;
     names fn_actual_names = header.m_fn_actual_names;
-    for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
+    buffer<expr> fns;
+    for (unsigned fidx = 0; fidx < ues2.get_num_fns(); fidx++) {
+        expr const & fn = ues2.get_fn(fidx);
+        fns.push_back(fn);
+    }
+    for (unsigned fidx = 0; fidx < ues2.get_num_fns(); fidx++) {
         equations_header new_header = header;
         new_header.m_num_fns         = 1;
         new_header.m_fn_names        = names(head(fn_names));
@@ -61,22 +53,27 @@ static void split_rec_fns(type_context_old & ctx, expr const & e, buffer<expr> &
         fn_names                     = tail(fn_names);
         fn_actual_names              = tail(fn_actual_names);
         buffer<expr> eqns;
-        for (expr const & eqn : ues.get_eqns_of(fidx)) {
-            eqns.push_back(ctx.mk_lambda(ues.get_fn(fidx), eqn));
+        for (expr const & eqn : ues2.get_eqns_of(fidx)) {
+            unpack_eqn ue(ctx2, eqn);
+            expr new_rhs = replace_locals(ue.rhs(), fns, aux_rec_fns);
+            ue.rhs() = new_rhs;
+            eqns.push_back(ctx2.mk_lambda(ues2.get_fn(fidx), ue.repack()));
         }
         result.push_back(mk_equations(new_header, eqns.size(), eqns.data()));
     }
+
+    mctx = ctx2.mctx();
+    return new_lctx;
 }
 
-static expr fix_rec_apps(expr const & e, name_map<expr> const & name2new_type,
-                         buffer<expr> const & closure_params) {
+static expr fix_rec_apps(expr const & e, name_map<name> const & aux_rec_name2actual_name,
+                         levels const & closure_levels, buffer<expr> const & closure_params) {
     return replace(e, [&](expr const & t) {
-            if (is_rec_fn_macro(t)) {
-                if (auto new_type = name2new_type.find(get_rec_fn_name(t))) {
-                    return some_expr(mk_app(mk_rec_fn_macro(get_rec_fn_name(t), *new_type),
-                                            closure_params));
+            if (is_local(t)) {
+                if (name const * actual_name = aux_rec_name2actual_name.find(mlocal_name(t))) {
+                    return some_expr(mk_app(mk_constant(*actual_name, closure_levels), closure_params));
                 } else {
-                    throw exception("internal error, ill-formed mutual recursive definition");
+                    return none_expr();
                 }
             } else {
                 return none_expr();
@@ -87,12 +84,22 @@ static expr fix_rec_apps(expr const & e, name_map<expr> const & name2new_type,
 eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
                                   metavar_context & mctx, local_context const & lctx,
                                   expr const & e) {
-    type_context_old ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
-
-    /* Replace recursive application with macro, and split mutual definition in n definitions. */
-    expr e1 = replace_rec_apps(ctx, e);
+    /* Split recursive equations by using new auxiliary `.rec` locals */
+    buffer<expr> aux_rec_fns;
     buffer<expr> es;
-    split_rec_fns(ctx, e1, es);
+    local_context aux_lctx = split_rec_fns(env, mctx, lctx, e, aux_rec_fns, es);
+    type_context_old ctx(env, mctx, aux_lctx, elab.get_cache(), transparency_mode::Semireducible);
+
+    /* Create set of auxiliary locals and mapping from auxiliary local to actual name */
+    equations_header const & header = get_equations_header(e);
+    name_set       aux_rec_fn_names;
+    name_map<name> aux_rec_fn_name2actual_name;
+    names fn_actual_names = header.m_fn_actual_names;
+    for (expr const & aux_rec_fn : aux_rec_fns) {
+        aux_rec_fn_names.insert(mlocal_name(aux_rec_fn));
+        aux_rec_fn_name2actual_name.insert(mlocal_name(aux_rec_fn), head(fn_actual_names));
+        fn_actual_names = tail(fn_actual_names);
+    }
 
     if (is_recursive_eqns(ctx, e)) {
         /* We create auxiliary definitions when compiling mutually recursive equations. */
@@ -102,83 +109,84 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
         closure_helper helper(ctx);
 
         /* 1. Compile pattern matching */
-
         for (unsigned fidx = 0; fidx < es.size(); fidx++) {
             unpack_eqns ues(ctx, es[fidx]);
-            auto R = elim_match(env, elab, mctx, lctx, es[fidx]);
-            fns.push_back(helper.collect(R.m_fn));
+            auto R = elim_match(env, elab, mctx, aux_lctx, es[fidx]);
+
+            /* We must not collect auxiliary locals in `aux_rec_fns` */
+            fns.push_back(helper.collect(R.m_fn, aux_rec_fn_names));
             fn_types.push_back(helper.collect(ctx.infer(ues.get_fn(0))));
             for (list<expr> const & ts : R.m_counter_examples) {
                 counter_examples.push_back(mk_app(ues.get_fn(0), ts));
             }
         }
-
         helper.finalize_collection();
 
-        buffer<level> closure_lvl_params;
-        buffer<expr>  closure_params;
-        helper.get_level_closure(closure_lvl_params);
-        helper.get_expr_closure(closure_params);
+        buffer<level> closure_lvl_args;
+        buffer<expr>  closure_args;
+        helper.get_level_closure(closure_lvl_args);
+        helper.get_expr_closure(closure_args);
 
         names lvl_names;
         lvl_names = helper.get_norm_level_names();
+        levels lvls = param_names_to_levels(lvl_names);
+        buffer<expr> const & params = helper.get_norm_closure_params();
 
-        equations_header const & header = get_equations_header(e);
-        names fn_names             = header.m_fn_names;
-        names fn_actual_names      = header.m_fn_actual_names;
-        bool zeta                       = get_eqn_compiler_zeta(elab.get_options());
+        bool zeta = get_eqn_compiler_zeta(elab.get_options());
 
         /* 2. Update fn_types.
            zeta-expand (if needed) and apply closures. */
-
-        name_map<expr> name2type;
         for (unsigned fidx = 0; fidx < es.size(); fidx++) {
-            name fn_name = head(fn_actual_names);
             expr fn_type = fn_types[fidx];
             if (zeta) {
-                fn_type = zeta_expand(lctx, fn_type);
+                fn_type = zeta_expand(aux_lctx, fn_type);
             }
             fn_type   = helper.mk_pi_closure(fn_type);
-            fn_types[fidx] = fn_type;
-            name2type.insert(fn_name, fn_type);
-            fn_actual_names   = tail(fn_actual_names);
+            fn_types[fidx]  = fn_type;
         }
 
-        /* 3. Fix recursive applications, declare definition, and private/alias info */
-
+        /* 3. Fix recursive applications, and create definitions */
+        buffer<declaration> new_declarations;
         fn_actual_names      = header.m_fn_actual_names;
-        buffer<expr> result_fns;
         for (unsigned fidx = 0; fidx < es.size(); fidx++) {
             name fn_name = head(fn_actual_names);
             expr fn_type = fn_types[fidx];
             expr fn      = fns[fidx];
             if (zeta) {
-                fn      = zeta_expand(lctx, fn);
+                fn      = zeta_expand(aux_lctx, fn);
             }
-            fn = fix_rec_apps(fn, name2type, helper.get_norm_closure_params());
+            fn = fix_rec_apps(fn, aux_rec_fn_name2actual_name, lvls, params);
             fn = helper.mk_lambda_closure(fn);
 
             bool use_self_opt = true;
             bool is_meta      = true;
             declaration d     = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, is_meta);
-            env               = module::add(env, check(env, d));
 
-            expr result_fn    = mk_app(mk_constant(fn_name, levels(closure_lvl_params)), closure_params);
+            new_declarations.push_back(d);
+            fn_actual_names   = tail(fn_actual_names);
+        }
+
+        env = module::add_meta(env, new_declarations);
+
+        /* 4. Create result and add private/alias info */
+        buffer<expr> result_fns;
+        names fn_names       = header.m_fn_names;
+        fn_actual_names      = header.m_fn_actual_names;
+        for (unsigned fidx = 0; fidx < es.size(); fidx++) {
+            name fn_name = head(fn_actual_names);
+            expr result_fn    = mk_app(mk_constant(fn_name, levels(closure_lvl_args)), closure_args);
 
             result_fns.push_back(result_fn);
-
             if (header.m_is_private) {
                 env = register_private_name(env, head(fn_names), fn_name);
                 env = add_expr_alias(env, head(fn_names), fn_name);
             }
-
-            fn_names          = tail(fn_names);
-            fn_actual_names   = tail(fn_actual_names);
+            fn_names        = tail(fn_names);
+            fn_actual_names = tail(fn_actual_names);
         }
 
-        /* 4. Compile. Remark: we need a separate pass because we need to reserve the functions
+        /* 5. Compile. Remark: we need a separate pass because we need to reserve the functions
            and their arities in the VM. */
-
         buffer<declaration> new_decls;
         for (name const & n : header.m_fn_actual_names) {
             new_decls.push_back(env.get(n));
@@ -192,8 +200,9 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
                 ss << " '" << n << "'";
             throw nested_exception(ss, ex);
         }
+
         return { to_list(result_fns), to_list(counter_examples) };
-    } else {
+    } else  {
         lean_assert(!is_recursive_eqns(ctx, e));
         /* If the equations are recursive, we simply compile each one of them and combine the
            results.
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 81dd04e756..44298db566 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -977,7 +977,7 @@ void update_telescope(type_context_old & ctx, buffer<expr> const & vars, expr co
 }
 
 /* Helper functor for mk_smart_unfolding_definition */
-struct replace_rec_fn_macro_fn : public replace_visitor {
+struct replace_aux_meta_fn : public replace_visitor {
     name const & m_fn_aux_name;
     expr const & m_new_fn;
     unsigned     m_nargs_to_skip;
@@ -986,8 +986,8 @@ struct replace_rec_fn_macro_fn : public replace_visitor {
     virtual expr visit_app(expr const & e) override {
         buffer<expr> args;
         expr const & fn = get_app_args(e, args);
-        if (is_rec_fn_macro(fn)) {
-            if (args.size() >= m_nargs_to_skip && get_rec_fn_name(fn) == m_fn_aux_name) {
+        if (is_constant(fn) && const_name(fn) == m_fn_aux_name) {
+            if (args.size() >= m_nargs_to_skip) {
                 m_found = true;
                 for (unsigned i = m_nargs_to_skip; i < args.size(); i++) {
                     expr & arg   = args[i];
@@ -1013,7 +1013,7 @@ struct replace_rec_fn_macro_fn : public replace_visitor {
         }
     }
 
-    replace_rec_fn_macro_fn(name const & fn_aux_name, expr const & new_fn, unsigned nargs_to_skip):
+    replace_aux_meta_fn(name const & fn_aux_name, expr const & new_fn, unsigned nargs_to_skip):
         m_fn_aux_name(fn_aux_name),
         m_new_fn(new_fn),
         m_nargs_to_skip(nargs_to_skip) {
@@ -1050,7 +1050,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const
         expr new_fn  = mk_app(mk_constant(n, ls), locals.size(), locals.data());
         helper_value = instantiate_value_univ_params(*aux_d, const_levels(fn));
         helper_value = apply_beta(helper_value, args.size(), args.data());
-        replace_rec_fn_macro_fn proc(meta_aux_fn_name, new_fn, args.size());
+        replace_aux_meta_fn proc(meta_aux_fn_name, new_fn, args.size());
         helper_value = proc(helper_value);
         if (!proc.m_found)
             throw exception("failed to generate helper declaration for smart unfolding, auxiliary meta declaration does not contain recursive application");