diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp
index d2dceb6832..e593f9281d 100644
--- a/src/library/compiler/elim_recursors.cpp
+++ b/src/library/compiler/elim_recursors.cpp
@@ -178,9 +178,8 @@ protected:
                 type_context::tmp_locals minor_locals(m_ctx);
                 buffer<expr> minor_recs; /* "recursive calls" */
                 lean_assert(carity >= nparams);
-                unsigned num_recursive = get_num_inductive_hypotheses_for(env(), cnames[i]);
-                lean_assert(num_recursive <= carity - nparams);
-                unsigned num_nonrecursive = carity - nparams - num_recursive;
+                buffer<bool> rec_mask;
+                get_constructor_rec_arg_mask(env(), cnames[i], rec_mask);
                 for (unsigned j = 0; j < carity - nparams; j++) {
                     minor            = ctx().whnf(minor);
                     lean_assert(is_lambda(minor));
@@ -194,7 +193,7 @@ protected:
                         expr aux_local = aux_locals.push_local_from_binding(minor_local_type);
                         minor_local_type = ctx().whnf(instantiate(binding_body(minor_local_type), aux_local));
                     }
-                    if (j >= num_nonrecursive) {
+                    if (rec_mask[nparams + j]) {
                         /* Recursive data, we must update minor_recs */
                         buffer<expr> I_args;
                         get_app_args(minor_local_type, I_args);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 7551c4bbb6..aeffa1b16e 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -285,8 +285,9 @@ unsigned get_constructor_idx(environment const & env, name const & n) {
     lean_unreachable();
 }
 
-unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n) {
+unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n, buffer<bool> & rec_mask) {
     lean_assert(inductive::is_intro_rule(env, n));
+    lean_assert(rec_mask.empty());
     name I_name = *inductive::is_intro_rule(env, n);
     inductive::inductive_decl decl = *inductive::is_inductive_decl(env, I_name);
     expr type   = env.get(n).get_type();
@@ -300,13 +301,26 @@ unsigned get_num_inductive_hypotheses_for(environment const & env, name const &
                     }
                     return false;
                 })) {
+
             r++;
+            rec_mask.push_back(true);
+        } else {
+            rec_mask.push_back(false);
         }
         type = binding_body(type);
     }
     return r;
 }
 
+unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n) {
+    buffer<bool> rec_mask;
+    return get_num_inductive_hypotheses_for(env, n, rec_mask);
+}
+
+void get_constructor_rec_arg_mask(environment const & env, name const & n, buffer<bool> & rec_mask) {
+    get_num_inductive_hypotheses_for(env, n, rec_mask);
+}
+
 expr instantiate_univ_param (expr const & e, name const & p, level const & l) {
     return instantiate_univ_params(e, to_list(p), to_list(l));
 }
diff --git a/src/library/util.h b/src/library/util.h
index 592d602345..a2ce8dd43f 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -96,6 +96,13 @@ unsigned get_constructor_idx(environment const & env, name const & n);
     hypotheses. This function return then number of inductive hypotheses for the minor premise associated with
     the constructor named \c n. */
 unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n);
+/** Given a constructor \c n, store in the bitmask rec_mask[i] = true iff the i-th argument
+    of \c n is recursive.
+
+    \pre is_intro_rule(n) && rec_mask.empty() */
+void get_constructor_rec_arg_mask(environment const & env, name const & n, buffer<bool> & rec_mask);
+/** Combines get_num_inductive_hypotheses_for and get_constructor_rec_arg_mask */
+unsigned get_num_inductive_hypotheses_for(environment const & env, name const & n, buffer<bool> & rec_mask);
 
 /* Store in `rec_args` the recursive arguments of constructor application \c `e`.
    The result is false if `e` is not a constructor application.