diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt
index df179a6559..8ae692bce6 100644
--- a/src/library/compiler/CMakeLists.txt
+++ b/src/library/compiler/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(compiler OBJECT old_util.cpp eta_expansion.cpp preprocess.cpp
-  compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
+  compiler_step_visitor.cpp comp_irrelevant.cpp
   inliner.cpp erase_irrelevant.cpp reduce_arity.cpp
   lambda_lifting.cpp simp_inductive.cpp nat_value.cpp
   vm_compiler.cpp old_cse.cpp elim_unused_lets.cpp extract_values.cpp init_module.cpp
diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp
deleted file mode 100644
index 18f08982d6..0000000000
--- a/src/library/compiler/elim_recursors.cpp
+++ /dev/null
@@ -1,320 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/type_checker.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
-#include "kernel/for_each_fn.h"
-#include "library/locals.h"
-#include "library/module.h"
-#include "library/util.h"
-#include "library/trace.h"
-#include "library/compiler/old_util.h"
-#include "library/compiler/procedure.h"
-#include "library/compiler/comp_irrelevant.h"
-#include "library/compiler/compiler_step_visitor.h"
-
-namespace lean {
-static name * g_rec_arg_fresh = nullptr;
-
-/* Store in `rec_args` the recursive arguments of constructor application \c `e`.
-   The result is false if `e` is not a constructor application.
-   The unsigned value at rec_args represents the arity of the recursive argument.
-   The value is only greater than zero for reflexive inductive datatypes such as:
-
-      inductive inftree (A : Type)
-      | leaf : A → inftree
-      | node : (nat → inftree) → inftree
-
-  \pre `n` is a constructor name.
-
-  \remark This method does not support nested or mutual inductive datatypes. */
-static void get_constructor_rec_arg_mask(environment const & env, name const & n, buffer<bool> & rec_mask) {
-    lean_assert(rec_mask.empty());
-    constant_info info = env.get(n);
-    lean_assert(info.is_constructor());
-    local_ctx lctx;
-    name_generator ngen(*g_rec_arg_fresh);
-    name I_name = info.to_constructor_val().get_induct();
-    expr type   = type_checker(env).whnf(info.get_type());
-    while (is_pi(type)) {
-        expr dom = type_checker(env, lctx).whnf(binding_domain(type));
-        while (is_pi(dom)) {
-            expr local = lctx.mk_local_decl(ngen, binding_name(dom), binding_domain(dom));
-            dom = type_checker(env, lctx).whnf(instantiate(binding_body(dom), local));
-        }
-        auto fn = get_app_fn(dom);
-        if (is_constant(fn) && const_name(fn) == I_name) {
-            rec_mask.push_back(true);
-        } else {
-            rec_mask.push_back(false);
-        }
-        expr local = lctx.mk_local_decl(ngen, binding_name(type), binding_domain(type));
-        type = type_checker(env, lctx).whnf(instantiate(binding_body(type), local));
-    }
-}
-
-class elim_recursors_fn : public compiler_step_visitor {
-    name                m_prefix;
-    unsigned            m_idx;
-    buffer<procedure> & m_new_decls;
-protected:
-    expr declare_aux_def(name const & n, expr const & value) {
-        m_new_decls.emplace_back(n, optional<pos_info>(), value);
-        /* We should use a new type checker because m_env is updated by this object.
-           It is safe to use type_checker because value does not contain free variables. */
-        names ps = to_names (collect_univ_params(value));
-        type_checker tc(m_env);
-        expr type         = tc.infer(value);
-        bool meta         = true;
-        /* We add declaration as an axiom to make sure
-           we can infer the type of the resultant expression. */
-        m_env = m_env.add(mk_axiom(n, ps, type, meta));
-        return mk_constant(n, lparams_to_levels(ps));
-    }
-
-    typedef rb_map<unsigned, local_decl, unsigned_rev_cmp> idx2decls;
-
-    void collect_locals(expr const & e, idx2decls & r) {
-        local_context const & lctx = ctx().lctx();
-        for_each(e, [&](expr const & e, unsigned) {
-                if (is_local_decl_ref(e)) {
-                    local_decl d = lctx.get_local_decl(e);
-                    r.insert(d.get_idx(), d);
-                }
-                return true;
-            });
-    }
-
-    expr abstract_locals(expr e, buffer<expr> & locals) {
-        idx2decls map;
-        collect_locals(e, map);
-        if (map.empty()) {
-            return e;
-        } else {
-            while (!map.empty()) {
-                /* remove local_decl with biggest idx */
-                local_decl d = map.erase_min();
-                expr l       = d.mk_ref();
-                if (auto v = d.get_value()) {
-                    collect_locals(*v, map);
-                    e = instantiate(abstract(e, l), *v);
-                } else {
-                    collect_locals(d.get_type(), map);
-                    if (is_comp_irrelevant(ctx(), l))
-                        locals.push_back(mark_comp_irrelevant(l));
-                    else
-                        locals.push_back(l);
-                    e = abstract(e, l);
-                    e = mk_lambda(d.get_name(), d.get_type(), e);
-                }
-            }
-            return e;
-        }
-    }
-
-    expr consume_lambdas(type_context_old::tmp_locals & locals, expr e) {
-        while (true) {
-            expr new_e = ctx().whnf(e);
-            if (is_lambda(new_e)) {
-                e = new_e;
-                expr local = locals.push_local_from_binding(e);
-                e = instantiate(binding_body(e), local);
-            } else {
-                return head_beta_reduce(e);
-            }
-        }
-    }
-
-    /* Process recursor application of recursive datatype.
-       We create a auxiliary recursive definition using cases_on and rec_fn_macro. */
-    expr visit_recursor_app(expr const & e) {
-        buffer<expr> args;
-        expr const & fn = get_app_args(e, args);
-        name const & rec_name     = const_name(fn);
-        name const & I_name       = rec_name.get_prefix();
-        constant_info rec_info    = env().get(rec_name);
-        recursor_val rec_val      = rec_info.to_recursor_val();
-        if (rec_val.get_nmotives() != 1) {
-            throw exception(sstream() << "failed to generate code for '" << rec_name << "', code generator currently does support recursors with more than one motive");
-        }
-        unsigned nparams          = rec_val.get_nparams();
-        unsigned nminors          = rec_val.get_nminors();
-        unsigned nindices         = rec_val.get_nindices();
-        unsigned first_minor_idx  = nparams + 1;
-        /* Create auxiliary application containing params + typeformer + minor premises.
-           This application is going to be the base of the auxiliary recursive definition. */
-        expr aux = mk_app(fn, nparams + 1 + nminors, args.data());
-        /* Abstract locals (and let values) occurring in aux */
-        buffer<expr> abst_locals;
-        aux = abstract_locals(aux, abst_locals);
-        /* 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_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. */
-        type_context_old::tmp_locals locals(m_ctx);
-        buffer<expr> aux_decl_params; /* "fixed" parameters of the auxiliary recursive declaration. */
-        expr aux_body = aux;
-        while (is_lambda(aux_body)) {
-            expr d = instantiate_rev(binding_domain(aux_body), locals.size(), locals.data());
-            expr p = locals.push_local(binding_name(aux_body), d, binding_info(aux_body));
-            aux_decl_params.push_back(p);
-            aux_body = binding_body(aux_body);
-        }
-        aux_body = instantiate_rev(aux_body, locals.size(), locals.data());
-        lean_assert(is_app(aux_body) && is_constant(get_app_fn(aux_body), rec_name));
-        buffer<expr> aux_body_args;
-        get_app_args(aux_body, aux_body_args);
-        /* Update rec_fn, create an application using aux_decl_params.
-           These parameters are fixed in recursive calls. */
-        rec_fn = mk_app(rec_fn, aux_decl_params);
-        /* Create locals for indices and major premise */
-        expr aux_body_type = ctx().infer(aux_body);
-        buffer<expr> indices;
-        for (unsigned i = 0; i < nindices; i++) {
-            aux_body_type = ctx().whnf(aux_body_type);
-            lean_assert(is_pi(aux_body_type));
-            expr index = locals.push_local_from_binding(aux_body_type);
-            indices.push_back(index);
-            aux_body_type = instantiate(binding_body(aux_body_type), index);
-        }
-        aux_body_type = ctx().whnf(aux_body_type);
-        lean_assert(is_pi(aux_body_type));
-        expr major = locals.push_local_from_binding(aux_body_type);
-        /* Make sure result is eta-expanded */
-        buffer<expr> extra_args; /* to make sure result is eta-expanded */
-        aux_body_type = instantiate(binding_body(aux_body_type), major);
-        while (true) {
-            aux_body_type = ctx().whnf(aux_body_type);
-            if (!is_pi(aux_body_type))
-                break;
-            expr new_arg = locals.push_local_from_binding(aux_body_type);
-            extra_args.push_back(new_arg);
-            aux_body_type = instantiate(binding_body(aux_body_type), new_arg);
-        }
-        /* Create auxiliary recursive function. It is a cases_on expression. */
-        buffer<expr> cases_on_args;
-        {
-            /* Add parameters and motive from aux_body_args */
-            cases_on_args.append(nparams + 1, aux_body_args.data());
-            /* Add indices */
-            cases_on_args.append(indices);
-            /* Add major */
-            cases_on_args.push_back(major);
-            /* Add minor premises */
-            buffer<name> cnames; /* constructor names */
-            get_constructor_names(env(), I_name, cnames);
-            for (unsigned i = 0; i < nminors; i++) {
-                // tout() << ">> cname: " << cnames[i] << "\n";
-                unsigned carity = get_constructor_arity(env(), cnames[i]);
-                expr minor      = aux_body_args[first_minor_idx + i];
-                // tout() << ">> minor: " << minor << "\n";
-                type_context_old::tmp_locals minor_locals(m_ctx);
-                buffer<expr> minor_recs; /* "recursive calls" */
-                lean_assert(carity >= nparams);
-                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));
-                    expr minor_local = minor_locals.push_local_from_binding(minor);
-                    minor = instantiate(binding_body(minor), minor_local);
-                    /* Check if minor_local is recursive data */
-                    type_context_old::tmp_locals aux_locals(m_ctx);
-                    expr minor_local_type = ctx().whnf(ctx().infer(minor_local));
-                    // tout() << ">>> minor_local_type: " << minor_local_type << "\n";
-                    while (is_pi(minor_local_type)) {
-                        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 (rec_mask[nparams + j]) {
-                        /* Recursive data, we must update minor_recs */
-                        buffer<expr> I_args;
-                        get_app_args(minor_local_type, I_args);
-                        lean_assert(I_args.size() == nparams + nindices);
-                        /* Construct term to replace the inductive/recursive hypothesis and add it to minor_recs.
-                           The term is of the form
-                              fun aux_locals, rec_fn I_args_indices (minor_local aux_locals)
-                        */
-                        expr rec_fn_indices = mk_app(rec_fn, nindices, I_args.data() + nparams);
-                        expr minor_rec = mk_app(rec_fn_indices, mk_app(minor_local, aux_locals.as_buffer()));
-                        minor_rec = aux_locals.mk_lambda(minor_rec);
-                        // tout() << ">> minor_rec: " << minor_rec << "\n";
-                        minor_recs.push_back(minor_rec);
-                    }
-                }
-                /* Replace recursive/inductive hypothesis with minor_recs */
-                for (expr const & minor_rec : minor_recs) {
-                    minor = ctx().whnf(minor);
-                    // tout() << ">> minor: " << minor << "\n";
-                    lean_assert(is_lambda(minor));
-                    minor = instantiate(binding_body(minor), minor_rec);
-                }
-                /* Keep consuming lambda */
-                minor = consume_lambdas(minor_locals, minor);
-                minor = visit(head_beta_reduce(minor));
-                minor = minor_locals.mk_lambda(minor);
-                cases_on_args.push_back(minor);
-            }
-        }
-        name cases_on_name  = name(I_name, "cases_on");
-        expr cases_on_fn    = mk_constant(cases_on_name, const_levels(fn));
-        expr cases_on       = mk_app(mk_app(cases_on_fn, cases_on_args), extra_args);
-        expr aux_decl_value = locals.mk_lambda(cases_on);
-        expr aux_decl_cnst  = declare_aux_def(aux_decl_name, aux_decl_value);
-        buffer<expr> rest_args;
-        for (unsigned i = nparams + 1 + nminors; i < args.size(); i++)
-            rest_args.push_back(visit(args[i]));
-        expr r = mk_app(mk_rev_app(aux_decl_cnst, abst_locals), rest_args);
-        return r;
-    }
-
-    bool is_recursive_recursor(name const & n) {
-        constant_info info = env().get(n);
-        if (!info.is_recursor())
-            return false;
-        return is_recursive_datatype(env(), info.to_recursor_val().get_induct());
-    }
-
-    virtual expr visit_app(expr const & e) override {
-        expr const & fn = get_app_fn(e);
-        if (is_constant(fn)) {
-            name const & n = const_name(fn);
-            if (is_recursor(env(), n) && is_recursive_recursor(n)) {
-                return visit_recursor_app(e);
-            }
-        }
-        return compiler_step_visitor::visit_app(head_beta_reduce(e));
-    }
-
-public:
-    elim_recursors_fn(environment const & env, abstract_context_cache & cache,
-                      name const & prefix, buffer<procedure> & new_decls):
-        compiler_step_visitor(env, cache), m_prefix(prefix), m_idx(1), m_new_decls(new_decls) {}
-
-    environment const & env() const { return m_env; }
-};
-
-expr elim_recursors(environment & env, abstract_context_cache & cache,
-                    name const & prefix, expr const & e, buffer<procedure> & new_decls) {
-    elim_recursors_fn fn(env, cache, prefix, new_decls);
-    expr new_e = fn(e);
-    env = fn.env();
-    return new_e;
-}
-
-void initialize_elim_recursors() {
-    g_rec_arg_fresh = new name("_rec_arg_fresh");
-    register_name_generator_prefix(*g_rec_arg_fresh);
-}
-
-void finalize_elim_recursors() {
-    delete g_rec_arg_fresh;
-}
-}
diff --git a/src/library/compiler/elim_recursors.h b/src/library/compiler/elim_recursors.h
deleted file mode 100644
index a93c160869..0000000000
--- a/src/library/compiler/elim_recursors.h
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-#include "library/compiler/procedure.h"
-namespace lean {
-/** \brief Eliminate recursor applications */
-expr elim_recursors(environment & env, abstract_context_cache & cache, name const & prefix, expr const & e, buffer<procedure> & new_decls);
-void initialize_elim_recursors();
-void finalize_elim_recursors();
-}
diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp
index e4003e5366..99d8f61270 100644
--- a/src/library/compiler/init_module.cpp
+++ b/src/library/compiler/init_module.cpp
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "library/compiler/inliner.h"
 #include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/simp_inductive.h"
-#include "library/compiler/elim_recursors.h"
 #include "library/compiler/vm_compiler.h"
 
 #include "library/compiler/lcnf.h"
@@ -26,7 +25,6 @@ void initialize_compiler_module() {
     initialize_erase_irrelevant();
     initialize_simp_inductive();
     initialize_vm_compiler();
-    initialize_elim_recursors();
     //======
     initialize_lcnf();
     initialize_elim_dead_let();
@@ -38,7 +36,6 @@ void finalize_compiler_module() {
     finalize_elim_dead_let();
     finalize_lcnf();
     //======
-    finalize_elim_recursors();
     finalize_vm_compiler();
     finalize_simp_inductive();
     finalize_erase_irrelevant();
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 5d0c11a383..fc24a34aac 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -29,7 +29,6 @@ Author: Leonardo de Moura
 #include "library/compiler/nat_value.h"
 #include "library/compiler/eta_expansion.h"
 #include "library/compiler/inliner.h"
-#include "library/compiler/elim_recursors.h"
 #include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/reduce_arity.h"
 #include "library/compiler/lambda_lifting.h"
@@ -288,6 +287,9 @@ public:
         lean_trace(name({"compiler", "input"}), tout() << d.get_name() << "\n";);
         if (compile_irrelevant(d, procs))
             return m_env;
+
+
+
         exec_new_compiler(d);
         expr v = d.get_value();
         v = remove_meta_rec(v);
@@ -306,10 +308,7 @@ public:
         lean_cond_assert("compiler", check(d, v));
         lean_trace(name({"compiler", "eta_expansion"}), tout() << "\n" << v << "\n";);
         name n = get_real_name(d.get_name());
-        v = elim_recursors(m_env, m_cache, n, v, procs);
         procs.emplace_back(n, optional<pos_info>(), v);
-        lean_cond_assert("compiler", check(d, procs.back().m_code));
-        lean_trace(name({"compiler", "elim_recursors"}), tout() << "\n"; display(procs););
         erase_irrelevant(procs);
         lean_trace(name({"compiler", "erase_irrelevant"}), tout() << "\n"; display(procs););
         reduce_arity(m_env, m_cache, procs);
@@ -357,7 +356,6 @@ void initialize_preprocess() {
     register_trace_class({"compiler", "expand_aux"});
     register_trace_class({"compiler", "eta_expansion"});
     register_trace_class({"compiler", "inline"});
-    register_trace_class({"compiler", "elim_recursors"});
     register_trace_class({"compiler", "erase_irrelevant"});
     register_trace_class({"compiler", "reduce_arity"});
     register_trace_class({"compiler", "erase_trivial_structures"});