diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index 5c9f8b3cc6..1a753656e6 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -204,13 +204,13 @@ public:
             unsigned max_idx    = get_max_fvar_idx(target);
             if (max_idx >= first_var_idx) {
                 expr target_type = cheap_beta_reduce(type_checker(m_st, m_lctx).infer(target));
-                expr unit        = mk_unit(mk_level_one());
-                expr unit_mk     = mk_unit_mk(mk_level_one());
+                expr unit        = mk_unit();
+                expr unit_mk     = mk_unit_mk();
                 expr new_val     = ::lean::mk_lambda("u", unit, target);
                 expr new_type    = ::lean::mk_arrow(unit, target_type);
                 expr new_fvar    = m_lctx.mk_local_decl(ngen(), mk_join_point_name(m_j.append_after(m_next_idx)), new_type, new_val);
                 new_fvar_names.insert(fvar_name(new_fvar));
-                expr jmp         = ::lean::mk_let("_j", target_type, mk_app(new_fvar, unit_mk), mk_bvar(0));
+                expr jmp         = mk_app(new_fvar, unit_mk);
                 if (is_let) {
                     /* We must insert new_fvar after fvar with idx == max_idx */
                     m_next_idx++;
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 123fe18d10..b7a9285d78 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -431,6 +431,17 @@ expr mk_unit_mk(level const & l) {
     return mk_constant(get_punit_star_name(), {l});
 }
 
+static expr * g_unit = nullptr;
+static expr * g_unit_mk = nullptr;
+
+expr mk_unit() {
+    return *g_unit;
+}
+
+expr mk_unit_mk() {
+    return *g_unit_mk;
+}
+
 expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) {
     level l1 = get_level(ctx, A);
     level l2 = get_level(ctx, B);
@@ -1020,6 +1031,8 @@ static std::string * g_version_string = nullptr;
 std::string const & get_version_string() { return *g_version_string; }
 
 void initialize_library_util() {
+    g_unit           = new expr(mk_constant(get_unit_name()));
+    g_unit_mk        = new expr(mk_constant(get_unit_star_name()));
     g_true           = new expr(mk_constant(get_true_name()));
     g_true_intro     = new expr(mk_constant(get_true_intro_name()));
     g_and            = new expr(mk_constant(get_and_name()));
@@ -1066,5 +1079,7 @@ void finalize_library_util() {
     delete g_and_elim_left;
     delete g_and_elim_right;
     delete g_tactic_unit;
+    delete g_unit_mk;
+    delete g_unit;
 }
 }
diff --git a/src/library/util.h b/src/library/util.h
index 7d1a466f4b..f2d77151b4 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -161,6 +161,8 @@ expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
 
 expr mk_unit(level const & l);
 expr mk_unit_mk(level const & l);
+expr mk_unit();
+expr mk_unit_mk();
 
 expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
 expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);