diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp
index b7fa2fb2a4..08dc59ef55 100644
--- a/src/kernel/quot.cpp
+++ b/src/kernel/quot.cpp
@@ -8,7 +8,7 @@ Quotient types.
 */
 #include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
-#include "kernel/abstract.h"
+#include "kernel/local_ctx.h"
 #include "kernel/inductive/inductive.h"
 
 namespace lean {
@@ -27,15 +27,16 @@ static void check_eq_type(environment const & env) {
     if (!decl) throw exception("failed to initialize quot module, environment does not have 'eq' type");
     if (length(decl->m_level_params) != 1)
         throw exception("failed to initialize quot module, unexpected number of universe params at 'eq' type");
+    local_ctx lctx;
     level u = mk_param_univ(head(decl->m_level_params));
-    expr alpha = mk_local("α", "α", mk_sort(u), mk_implicit_binder_info());
-    expr expected_eq_type = Pi(alpha, mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
+    expr alpha = lctx.mk_local_decl("α", "α", mk_sort(u), mk_implicit_binder_info());
+    expr expected_eq_type = lctx.mk_pi(alpha, mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
     if (decl->m_type != expected_eq_type)
         throw exception("failed to initialize quot module, 'eq' has an expected type");
     if (length(decl->m_intro_rules) != 1)
         throw exception("failed to initialize quot module, unexpected number of constructors for 'eq' type");
-    expr a = mk_local("a", alpha);
-    expr expected_eq_refl_type = Pi(alpha, Pi(a, mk_app(mk_constant("eq", {u}), alpha, a, a)));
+    expr a = lctx.mk_local_decl("a", alpha);
+    expr expected_eq_refl_type = lctx.mk_pi({alpha, a}, mk_app(mk_constant("eq", {u}), alpha, a, a));
     if (mlocal_type(head(decl->m_intro_rules)) != expected_eq_refl_type) {
         throw exception("failed to initialize quot module, unexpected type for 'eq' type constructor");
     }
@@ -45,44 +46,45 @@ environment quot_declare(environment const & env) {
     check_eq_type(env);
     environment new_env = env;
     name u_name("u");
+    local_ctx lctx;
     level u         = mk_param_univ(u_name);
     expr Sort_u     = mk_sort(u);
-    expr alpha      = mk_local("α", "α", Sort_u, mk_implicit_binder_info());
-    expr r          = mk_local("r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
+    expr alpha      = lctx.mk_local_decl("α", "α", Sort_u, mk_implicit_binder_info());
+    expr r          = lctx.mk_local_decl("r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
     /* constant {u} quot {α : Sort u} (r : α → α → Prop) : Sort u */
-    new_env = add_constant(new_env, *quot_consts::g_quot, {u_name}, Pi(alpha, Pi(r, Sort_u)));
+    new_env = add_constant(new_env, *quot_consts::g_quot, {u_name}, lctx.mk_pi({alpha, r}, Sort_u));
     expr quot_r     = mk_app(mk_constant(*quot_consts::g_quot, {u}), alpha, r);
-    expr a          = mk_local("a", alpha);
+    expr a          = lctx.mk_local_decl("a", alpha);
     /* constant {u} quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : @quot.{u} α r */
     new_env = add_constant(new_env, *quot_consts::g_quot_mk, {u_name},
-                           Pi(alpha, Pi(r, Pi(a, quot_r))));
+                           lctx.mk_pi({alpha, r, a}, quot_r));
     /* make r implicit */
-    r               = mk_local("r", "r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())), mk_implicit_binder_info());
+    r               = lctx.mk_local_decl("r", "r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())), mk_implicit_binder_info());
     name v_name("v");
     level v         = mk_param_univ(v_name);
     expr Sort_v     = mk_sort(v);
-    expr beta       = mk_local("β", "β", Sort_v, mk_implicit_binder_info());
-    expr f          = mk_local("f", mk_arrow(alpha, beta));
-    expr b          = mk_local("b", alpha);
+    expr beta       = lctx.mk_local_decl("β", "β", Sort_v, mk_implicit_binder_info());
+    expr f          = lctx.mk_local_decl("f", mk_arrow(alpha, beta));
+    expr b          = lctx.mk_local_decl("b", alpha);
     expr r_a_b      = mk_app(r, a, b);
     /* f a = f b */
     expr f_a_eq_f_b = mk_app(mk_constant("eq", {v}), beta, mk_app(f, a), mk_app(f, b));
     /* (∀ a b : α, r a b → f a = f b) */
-    expr sanity     = Pi(a, Pi(b, mk_arrow(r_a_b, f_a_eq_f_b)));
+    expr sanity     = lctx.mk_pi({a, b}, mk_arrow(r_a_b, f_a_eq_f_b));
     /* constant {u v} quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)
                                 : (∀ a b : α, r a b → f a = f b) →  @quot.{u} α r → β */
     new_env = add_constant(new_env, *quot_consts::g_quot_lift, {u_name, v_name},
-                           Pi(alpha, Pi(r, Pi(beta, Pi(f, mk_arrow(sanity, mk_arrow(quot_r, beta)))))));
+                           lctx.mk_pi({alpha, r, beta, f}, mk_arrow(sanity, mk_arrow(quot_r, beta))));
     /* {β : @quot.{u} α r → Prop} */
-    beta            = mk_local("β", "β", mk_arrow(quot_r, mk_Prop()), mk_implicit_binder_info());
+    beta            = lctx.mk_local_decl("β", "β", mk_arrow(quot_r, mk_Prop()), mk_implicit_binder_info());
     expr quot_mk_a  = mk_app(mk_constant(*quot_consts::g_quot_mk, {u}), alpha, r, a);
-    expr all_quot   = Pi(a, mk_app(beta, quot_mk_a));
-    expr q          = mk_local("q", quot_r);
+    expr all_quot   = lctx.mk_pi(a, mk_app(beta, quot_mk_a));
+    expr q          = lctx.mk_local_decl("q", quot_r);
     expr beta_q     = mk_app(beta, q);
     /* constant {u} quot.ind {α : Sort u} {r : α → α → Prop} {β : @quot.{u} α r → Prop}
                    : (∀ a : α, β (@quot.mk.{u} α r a)) → ∀ q : @quot.{u} α r, β q */
     new_env = add_constant(new_env, *quot_consts::g_quot_ind, {u_name},
-                           Pi(alpha, Pi(r, Pi(beta, mk_arrow(all_quot, Pi(q, beta_q))))));
+                           lctx.mk_pi({alpha, r, beta}, mk_arrow(all_quot, lctx.mk_pi(q, beta_q))));
     return new_env;
 }