diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 8694d83ab7..b399569866 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -436,7 +436,6 @@ public: expr visit_lambda(expr e, bool root) { lean_assert(is_lambda(e)); - e = type_checker(m_st, m_lctx).eta_expand(e); expr r; { flet save_lctx(m_lctx, m_lctx);