diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index a0de120f49..fe82c9cd72 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -205,7 +205,7 @@ environment compile(environment const & env, options const & opts, names cs) {
     trace_compiler(name({"compiler", "stage1"}), ds);
     environment new_env = cache_stage1(env, ds);
     std::tie(new_env, ds) = specialize(new_env, ds, cfg);
-    // lcnf_check_let_decls(new_env, ds);
+    lean_assert(lcnf_check_let_decls(new_env, ds));
     trace_compiler(name({"compiler", "specialize"}), ds);
     ds = apply(elim_dead_let, ds);
     trace_compiler(name({"compiler", "elim_dead_let"}), ds);
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 641e55cabb..f0d0b6465a 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -600,8 +600,11 @@ class lcnf_valid_let_decls_fn {
             if (is_irrelevant_type(m_st, m_lctx, new_type)) {
                 return some_expr(e);
             }
-            if (optional<expr> found = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data())))
+            expr new_val  = instantiate_rev(let_value(e), fvars.size(), fvars.data());
+            if (optional<expr> found = visit(new_val))
                 return found;
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), let_name(e), new_type, new_val);
+            fvars.push_back(new_fvar);
             e = let_body(e);
         }
         return visit(instantiate_rev(e, fvars.size(), fvars.data()));
@@ -632,9 +635,9 @@ optional<expr> lcnf_valid_let_decls(environment const & env, expr const & e) {
 bool lcnf_check_let_decls(environment const & env, comp_decl const & d) {
     if (optional<expr> v = lcnf_valid_let_decls(env, d.snd())) {
         tout() << "LCNF violation at " << d.fst() << "\n" << *v << "\n";
-        return true;
-    } else {
         return false;
+    } else {
+        return true;
     }
 }