From d54b86d16b7c71ee5326e25ea270335b2819b00e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Sep 2018 16:21:00 -0700
Subject: [PATCH] chore(library/type_context): remove
 `reduce_large_elim_recursor`

---
 src/library/type_context.cpp | 19 -------------------
 src/library/type_context.h   |  1 -
 2 files changed, 20 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 792fde715d..857896fd96 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -730,18 +730,6 @@ optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {
     }
 }
 
-optional<expr> type_context_old::reduce_large_elim_recursor(expr const & e) {
-    expr const & f = get_app_fn(e);
-    if (!is_constant(f))
-        return none_expr();
-    auto & fn = const_name(f);
-    if (fn == get_acc_rec_name()) {
-        transparency_scope scope(*this, transparency_mode::All);
-        return norm_ext(e);
-    }
-    return none_expr();
-}
-
 bool type_context_old::use_zeta() const {
     return m_zeta;
 }
@@ -751,8 +739,6 @@ optional<expr> type_context_old::reduce_recursor(expr const & e) {
         return r;
     if (auto r = reduce_aux_recursor(e))
         return r;
-    if (auto r = reduce_large_elim_recursor(e))
-        return r;
     return none_expr();
 }
 
@@ -849,11 +835,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
                 continue;
             }
 
-            if (auto r = reduce_large_elim_recursor(e)) {
-                e = *r;
-                continue;
-            }
-
             return e;
         } else {
             e = mk_rev_app(f, args.size(), args.data());
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 8fcd72fc42..003a2eab04 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -683,7 +683,6 @@ public:
         This method is useful when we want to normalize the expression until we get a particular symbol as the head symbol. */
     expr whnf_head_pred(expr const & e, std::function<bool(expr const &)> const & pred); // NOLINT
     optional<expr> reduce_aux_recursor(expr const & e);
-    optional<expr> reduce_large_elim_recursor(expr const & e);
     optional<expr> reduce_projection(expr const & e);
     optional<expr> reduce_proj(expr const & e);
     optional<expr> norm_ext(expr const & e);