diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp
index 73550a1e42..3a38f24968 100644
--- a/src/library/compiler/lambda_lifting.cpp
+++ b/src/library/compiler/lambda_lifting.cpp
@@ -45,7 +45,7 @@ class lambda_lifting_fn : public compiler_step_visitor {
         type_context_old::tmp_locals locals(m_ctx);
         expr t = e;
         while (is_lambda(t)) {
-            lean_assert(is_neutral_expr(binding_domain(t)) || !has_loose_bvars(binding_domain(t)));
+            lean_assert(is_enf_neutral(binding_domain(t)) || !has_loose_bvars(binding_domain(t)));
             locals.push_local(binding_name(t), binding_domain(t), binding_info(t));
             t = binding_body(t);
         }
@@ -125,7 +125,7 @@ class lambda_lifting_fn : public compiler_step_visitor {
         type_context_old::tmp_locals locals(m_ctx);
         expr t = e;
         while (is_let(t)) {
-            lean_assert(is_neutral_expr(let_type(t)) || !has_loose_bvars(let_type(t)));
+            lean_assert(is_enf_neutral(let_type(t)) || !has_loose_bvars(let_type(t)));
             expr v = visit(instantiate_rev(let_value(t), locals.size(), locals.data()));
             locals.push_let(let_name(t), let_type(t), v);
             t = let_body(t);