diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 8b4b6a66e2..f2bd65743b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -958,14 +958,14 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
         throw elaborator_exception(ref, "invalid occurrence of field notation");
     expr r;
     switch (fn.kind()) {
-    case expr_kind::Var:
+    case expr_kind::BVar:
     case expr_kind::Pi:
     case expr_kind::Meta:
     case expr_kind::Sort:
         throw elaborator_exception(ref, "invalid application, function expected");
     // The expr_kind::App case can only happen when nary notation is used
     case expr_kind::App:       r = visit(fn, expected_type); break;
-    case expr_kind::Local:     r = fn; break;
+    case expr_kind::FVar:      r = fn; break;
     case expr_kind::Constant:  r = visit_const_core(fn); break;
     case expr_kind::Macro:     r = visit_macro(fn, expected_type, true); break;
     case expr_kind::Lambda:    r = visit_lambda(fn, expected_type); break;
@@ -3634,12 +3634,12 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
             return visit(get_annotation_arg(e), expected_type);
         } else {
             switch (e.kind()) {
-                case expr_kind::Var: lean_unreachable();  // LCOV_EXCL_LINE
+                case expr_kind::BVar: lean_unreachable();  // LCOV_EXCL_LINE
                 case expr_kind::Meta:
                     return e;
                 case expr_kind::Sort:
                     return copy_pos(e, visit_sort(e));
-                case expr_kind::Local:
+                case expr_kind::FVar:
                     return copy_pos(e, visit_local(e, expected_type));
                 case expr_kind::Constant:
                     return copy_pos(e, visit_constant(e, expected_type));
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 298b6b7469..602dca0e1c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -275,7 +275,7 @@ expr parser::rec_save_pos(expr const & e, pos_info p) {
 expr parser::copy_with_new_pos(expr const & e, pos_info p) {
     switch (e.kind()) {
     case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:
-    case expr_kind::Var:  case expr_kind::Local:
+    case expr_kind::BVar: case expr_kind::FVar:
         return save_pos(copy(e), p);
     case expr_kind::App:
         return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
@@ -1719,7 +1719,7 @@ struct to_pattern_fn {
 
 static expr quote(expr const & e) {
     switch (e.kind()) {
-        case expr_kind::Var:
+        case expr_kind::BVar:
             return mk_app(mk_constant({"expr", "var"}), quote(var_idx(e)));
         case expr_kind::Sort:
             return mk_app(mk_constant({"expr", "sort"}), mk_expr_placeholder());
@@ -1727,7 +1727,7 @@ static expr quote(expr const & e) {
             return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
         case expr_kind::Meta:
             return mk_expr_placeholder();
-        case expr_kind::Local:
+        case expr_kind::FVar:
             throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
                                                     << mlocal_pp_name(e) << "'");
         case expr_kind::App:
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
old mode 100755
new mode 100644
index 9a681c6d7e..462b5b6c7f
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1771,11 +1771,11 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
         if (auto k = to_unsigned(e))
             return format(*k);
     switch (e.kind()) {
-    case expr_kind::Var:       return pp_var(e);
+    case expr_kind::BVar:      return pp_var(e);
+    case expr_kind::FVar:      return pp_local(e);
     case expr_kind::Sort:      return pp_sort(e);
     case expr_kind::Constant:  return pp_const(e);
     case expr_kind::Meta:      return pp_meta(e);
-    case expr_kind::Local:     return pp_local(e);
     case expr_kind::App:       return pp_app(e);
     case expr_kind::Lambda:    return pp_lambda(e);
     case expr_kind::Pi:        return pp_pi(e);
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index 348b3466f9..ae816bcf88 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -67,14 +67,14 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) {
     check_system("expression equivalence test");
     bool result = false;
     switch (a.kind()) {
-    case expr_kind::Var:
+    case expr_kind::BVar:
         lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Constant:
         result =
             const_name(a) == const_name(b) &&
             compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
         break;
-    case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Meta: case expr_kind::FVar:
         result =
             mlocal_name(a) == mlocal_name(b) &&
             is_equiv_core(mlocal_type(a), mlocal_type(b));
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 37bf1e12db..efeb17813e 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -122,7 +122,7 @@ bool is_meta(expr const & e) {
 
 // Expr variables
 expr_var::expr_var(unsigned idx):
-    expr_cell(expr_kind::Var, idx, false, false, false, false),
+    expr_cell(expr_kind::BVar, idx, false, false, false, false),
     m_vidx(idx) {
     if (idx == std::numeric_limits<unsigned>::max())
         throw exception("invalid bound variable index, de Bruijn index is too big");
@@ -148,7 +148,7 @@ unsigned binder_info::hash() const {
 
 // Expr metavariables and local variables
 expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t):
-    expr_composite(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
+    expr_composite(is_meta ? expr_kind::Meta : expr_kind::FVar, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
                    !is_meta || t.has_local(), t.has_param_univ(),
                    1, get_loose_bvar_range(t)),
     m_name(n),
@@ -410,10 +410,10 @@ void expr_cell::dealloc() {
             #endif
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
-            case expr_kind::Var:        static_cast<expr_var*>(it)->dealloc(); break;
+            case expr_kind::BVar:       static_cast<expr_var*>(it)->dealloc(); break;
             case expr_kind::Macro:      static_cast<expr_macro*>(it)->dealloc(todo); break;
             case expr_kind::Meta:       static_cast<expr_mlocal*>(it)->dealloc(todo); break;
-            case expr_kind::Local:      static_cast<expr_local*>(it)->dealloc(todo); break;
+            case expr_kind::FVar:       static_cast<expr_local*>(it)->dealloc(todo); break;
             case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(); break;
             case expr_kind::Sort:       static_cast<expr_sort*>(it)->dealloc(); break;
             case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
@@ -532,8 +532,8 @@ expr mk_Type() { return *g_Type1; }
 
 unsigned get_weight(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Constant: case expr_kind::Sort:
-    case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::BVar:  case expr_kind::Constant: case expr_kind::Sort:
+    case expr_kind::Meta: case expr_kind::FVar:
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:  case expr_kind::Macro:
     case expr_kind::App:    case expr_kind::Let:
@@ -544,8 +544,8 @@ unsigned get_weight(expr const & e) {
 
 unsigned get_depth(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Constant: case expr_kind::Sort:
-    case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
+    case expr_kind::Meta: case expr_kind::FVar:
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:  case expr_kind::Macro:
     case expr_kind::App:    case expr_kind::Let:
@@ -632,12 +632,12 @@ expr update_let(expr const & e, expr const & new_type, expr const & new_value, e
 bool is_atomic(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Constant: case expr_kind::Sort:
-    case expr_kind::Var:
+    case expr_kind::BVar:
         return true;
     case expr_kind::Macro:
         return to_macro(e)->get_num_args() == 0;
     case expr_kind::App:      case expr_kind::Meta:
-    case expr_kind::Local:    case expr_kind::Lambda:
+    case expr_kind::FVar:     case expr_kind::Lambda:
     case expr_kind::Pi:       case expr_kind::Let:
         return false;
     }
@@ -786,11 +786,11 @@ unsigned hash_bi(expr const & e) {
 
 std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
     switch (k) {
-    case expr_kind::Var:      out << "Var"; break;
+    case expr_kind::BVar:     out << "Var"; break;
     case expr_kind::Sort:     out << "Sort"; break;
     case expr_kind::Constant: out << "Constant"; break;
     case expr_kind::Meta:     out << "Meta"; break;
-    case expr_kind::Local:    out << "Local"; break;
+    case expr_kind::FVar:     out << "Local"; break;
     case expr_kind::App:      out << "App"; break;
     case expr_kind::Lambda:   out << "Lambda"; break;
     case expr_kind::Pi:       out << "Pi"; break;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 8f2387dafb..57db6c0c20 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -29,18 +29,18 @@ class abstract_type_context;
 class expr;
 /* =======================================
    Expressions
-   expr ::=   Var           idx
+   expr ::=   BVar          idx
+          |   FVar          name
           |   Sort          level
           |   Constant      name [levels]
           |   Meta          name expr
-          |   Local         name expr
           |   App           expr expr
           |   Lambda        name expr expr
           |   Pi            name expr expr
           |   Let           name expr expr expr
           |   Macro         macro
 */
-enum class expr_kind { Var, Local, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro };
+enum class expr_kind { BVar, FVar, Sort, Constant, Meta, App, Lambda, Pi, Let, Macro };
 class expr_cell {
 protected:
     // The bits of the following field mean:
@@ -414,9 +414,9 @@ public:
 
 // =======================================
 // Testers
-inline bool is_var(expr_ptr e)         { return e->kind() == expr_kind::Var; }
+inline bool is_var(expr_ptr e)         { return e->kind() == expr_kind::BVar; }
 inline bool is_constant(expr_ptr e)    { return e->kind() == expr_kind::Constant; }
-inline bool is_local(expr_ptr e)       { return e->kind() == expr_kind::Local; }
+inline bool is_local(expr_ptr e)       { return e->kind() == expr_kind::FVar; }
 inline bool is_metavar(expr_ptr e)     { return e->kind() == expr_kind::Meta; }
 inline bool is_macro(expr_ptr e)       { return e->kind() == expr_kind::Macro; }
 inline bool is_app(expr_ptr e)         { return e->kind() == expr_kind::App; }
@@ -561,7 +561,7 @@ unsigned get_depth(expr const & e);
      occurring in \c e is in the interval <tt>[0, R)</tt>. */
 inline unsigned get_loose_bvar_range(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var:                            return var_idx(e) + 1;
+    case expr_kind::BVar:                           return var_idx(e) + 1;
     case expr_kind::Constant: case expr_kind::Sort: return 0;
     default:                                        return static_cast<expr_composite*>(e.raw())->m_loose_bvar_range;
     }
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 662a22a14e..9fbc35b877 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -70,7 +70,7 @@ class expr_eq_fn {
         if (m_cache.check(a, b))
             return true;
         switch (a.kind()) {
-        case expr_kind::Var:
+        case expr_kind::BVar:
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::Constant:
             return
@@ -81,7 +81,7 @@ class expr_eq_fn {
                 mlocal_name(a) == mlocal_name(b) &&
                 apply(mlocal_type(a), mlocal_type(b)) &&
                 (!CompareBinderInfo || mlocal_pp_name(a) == mlocal_pp_name(b));
-        case expr_kind::Local:
+        case expr_kind::FVar:
             return
                 mlocal_name(a) == mlocal_name(b) &&
                 apply(mlocal_type(a), mlocal_type(b)) &&
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index e7c66c52ca..b2ce33843a 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -70,7 +70,7 @@ class for_each_fn {
             unsigned offset = p.second;
 
             switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Var:
+            case expr_kind::Constant: case expr_kind::BVar:
             case expr_kind::Sort:
                 m_f(e, offset);
                 goto begin_loop;
@@ -85,10 +85,10 @@ class for_each_fn {
                 goto begin_loop;
 
             switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Var:
+            case expr_kind::Constant: case expr_kind::BVar:
             case expr_kind::Sort:
                 goto begin_loop;
-            case expr_kind::Meta: case expr_kind::Local:
+            case expr_kind::Meta: case expr_kind::FVar:
                 todo.emplace_back(mlocal_type(e), offset);
                 goto begin_loop;
             case expr_kind::Macro: {
diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp
index 3910657bae..2581cca020 100644
--- a/src/kernel/old_type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -214,8 +214,8 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
 
     expr r;
     switch (e.kind()) {
-    case expr_kind::Local: case expr_kind::Meta:  r = mlocal_type(e);  break;
-    case expr_kind::Var:
+    case expr_kind::FVar: case expr_kind::Meta:  r = mlocal_type(e);  break;
+    case expr_kind::BVar:
         lean_unreachable();  // LCOV_EXCL_LINE
     case expr_kind::Sort:
         if (!infer_only) check_level(sort_level(e));
@@ -283,7 +283,7 @@ expr old_type_checker::whnf_core(expr const & e) {
 
     // handle easy cases
     switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::BVar: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
         return e;
     case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
@@ -300,7 +300,7 @@ expr old_type_checker::whnf_core(expr const & e) {
     // do the actual work
     expr r;
     switch (e.kind()) {
-    case expr_kind::Var:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::BVar:  case expr_kind::Sort: case expr_kind::Meta: case expr_kind::FVar:
     case expr_kind::Pi:   case expr_kind::Constant: case expr_kind::Lambda:
         lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Macro:
@@ -386,7 +386,7 @@ optional<expr> old_type_checker::unfold_definition(expr const & e) {
 expr old_type_checker::whnf(expr const & e) {
     // Do not cache easy cases
     switch (e.kind()) {
-    case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
+    case expr_kind::BVar: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::FVar: case expr_kind::Pi:
         return e;
     case expr_kind::Lambda:   case expr_kind::Macro: case expr_kind::App:
     case expr_kind::Constant: case expr_kind::Let:
@@ -481,7 +481,7 @@ lbool old_type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use
             return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
         case expr_kind::Meta:
             lean_unreachable(); // LCOV_EXCL_LINE
-        case expr_kind::Var:      case expr_kind::Local: case expr_kind::App:
+        case expr_kind::BVar:      case expr_kind::FVar: case expr_kind::App:
         case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
             // We do not handle these cases in this method.
             break;
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 9f1bf3a7b5..d208eeebee 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -79,9 +79,9 @@ class replace_rec_fn {
             return save_result(e, offset, *r, shared);
         } else {
             switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Var:
+            case expr_kind::Constant: case expr_kind::Sort: case expr_kind::BVar:
                 return save_result(e, offset, e, shared);
-            case expr_kind::Meta:     case expr_kind::Local: {
+            case expr_kind::Meta:     case expr_kind::FVar: {
                 expr new_t = apply(mlocal_type(e), offset);
                 return save_result(e, offset, update_mlocal(e, new_t), shared);
             }
diff --git a/src/library/check.cpp b/src/library/check.cpp
index 4d5f42def7..2a102a1b67 100644
--- a/src/library/check.cpp
+++ b/src/library/check.cpp
@@ -108,13 +108,13 @@ struct check_fn {
             return;
         m_visited.insert(e);
         switch (e.kind()) {
-        case expr_kind::Local:
+        case expr_kind::FVar:
         case expr_kind::Meta:
         case expr_kind::Sort:
             break; /* do nothing */
         case expr_kind::Constant:
             return visit_constant(e);
-        case expr_kind::Var:
+        case expr_kind::BVar:
             lean_unreachable();  // LCOV_EXCL_LINE
         case expr_kind::Macro:
             return visit_macro(e);
diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index ea06de6464..206852ef02 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -48,9 +48,9 @@ class cse_fn : public compiler_step_visitor {
 
         void visit(expr const & e) {
             switch (e.kind()) {
-            case expr_kind::Var:      case expr_kind::Sort:
+            case expr_kind::BVar:      case expr_kind::Sort:
             case expr_kind::Meta:     case expr_kind::Pi:
-            case expr_kind::Constant: case expr_kind::Local:
+            case expr_kind::Constant: case expr_kind::FVar:
                 break;
             case expr_kind::Lambda:   visit_lambda(e); break;
             case expr_kind::Macro:    visit_macro(e); break;
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 349d8f8dae..68433a65a7 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -291,14 +291,14 @@ class vm_compiler_fn {
 
     void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         switch (e.kind()) {
-        case expr_kind::Var:      lean_unreachable();
+        case expr_kind::BVar:     lean_unreachable();
         case expr_kind::Sort:     lean_unreachable();
         case expr_kind::Meta:     lean_unreachable();
         case expr_kind::Pi:       lean_unreachable();
         case expr_kind::Lambda:   lean_unreachable();
         case expr_kind::Macro:    compile_macro(e, bpz, m);  break;
         case expr_kind::Constant: compile_constant(e);       break;
-        case expr_kind::Local:    compile_local(e, m);       break;
+        case expr_kind::FVar:     compile_local(e, m);       break;
         case expr_kind::App:      compile_app(e, bpz, m);    break;
         case expr_kind::Let:      compile_let(e, bpz, m);    break;
         }
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index 683f1f1113..5635a88e0b 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 namespace lean {
 expr copy(expr const & a) {
     switch (a.kind()) {
-    case expr_kind::Var:      return mk_var(var_idx(a));
+    case expr_kind::BVar:     return mk_var(var_idx(a));
     case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
     case expr_kind::Sort:     return mk_sort(sort_level(a));
     case expr_kind::Macro:    return mk_macro(to_macro(a)->m_definition, macro_num_args(a), macro_args(a));
@@ -19,7 +19,7 @@ expr copy(expr const & a) {
     case expr_kind::Lambda:   return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
     case expr_kind::Pi:       return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
     case expr_kind::Meta:     return mk_metavar(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a));
-    case expr_kind::Local:    return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
+    case expr_kind::FVar:     return mk_local(mlocal_name(a), mlocal_pp_name(a), mlocal_type(a), local_info(a));
     case expr_kind::Let:      return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 4b7f6c346d..3ca6f135cd 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -114,8 +114,8 @@ struct structural_rec_fn {
         /** \brief Return true iff all recursive applications in \c e are structurally smaller than \c m_pattern. */
         bool check_rhs(expr const & e) {
             switch (e.kind()) {
-            case expr_kind::Var:   case expr_kind::Meta:
-            case expr_kind::Local: case expr_kind::Constant:
+            case expr_kind::BVar: case expr_kind::Meta:
+            case expr_kind::FVar: case expr_kind::Constant:
             case expr_kind::Sort:
                 return true;
             case expr_kind::Macro:
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 7f614ec913..c292ff8e1e 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -21,7 +21,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
     }
     if (a == b)                          return false;
     switch (a.kind()) {
-    case expr_kind::Var:
+    case expr_kind::BVar:
         return var_idx(a) < var_idx(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
@@ -47,7 +47,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const *
             return is_lt(let_body(a), let_body(b), use_hash, lctx);
     case expr_kind::Sort:
         return is_lt(sort_level(a), sort_level(b), use_hash);
-    case expr_kind::Local:
+    case expr_kind::FVar:
         if (lctx) {
             if (auto d1 = lctx->find_local_decl(a))
             if (auto d2 = lctx->find_local_decl(b))
@@ -128,7 +128,7 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
     if (wa > wb)                         return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
     switch (a.kind()) {
-    case expr_kind::Var:
+    case expr_kind::BVar:
         return var_idx(a) < var_idx(b);
     case expr_kind::Constant:
         if (const_name(a) != const_name(b))
@@ -162,7 +162,7 @@ bool is_lt_no_level_params(expr const & a, expr const & b) {
             return is_lt_no_level_params(let_body(a), let_body(b));
     case expr_kind::Sort:
         return is_lt_no_level_params(sort_level(a), sort_level(b));
-    case expr_kind::Local: case expr_kind::Meta:
+    case expr_kind::FVar: case expr_kind::Meta:
         if (mlocal_name(a) != mlocal_name(b))
             return mlocal_name(a) < mlocal_name(b);
         else
diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp
index dac3500b35..8eed9fa288 100644
--- a/src/library/head_map.cpp
+++ b/src/library/head_map.cpp
@@ -26,14 +26,14 @@ head_index::head_index(expr const & e) {
 }
 
 int head_index::cmp::operator()(head_index const & i1, head_index const & i2) const {
-    if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Constant && i1.m_kind != expr_kind::Local))
+    if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Constant && i1.m_kind != expr_kind::FVar))
         return static_cast<int>(i1.m_kind) - static_cast<int>(i2.m_kind);
     else
         return quick_cmp(i1.m_name, i2.m_name);
 }
 
 std::ostream & operator<<(std::ostream & out, head_index const & head_idx) {
-    if (head_idx.m_kind == expr_kind::Constant || head_idx.m_kind == expr_kind::Local)
+    if (head_idx.m_kind == expr_kind::Constant || head_idx.m_kind == expr_kind::FVar)
         out << head_idx.m_name;
     else
         out << head_idx.m_kind;
diff --git a/src/library/head_map.h b/src/library/head_map.h
index 340b858530..c5e2723cd0 100644
--- a/src/library/head_map.h
+++ b/src/library/head_map.h
@@ -14,7 +14,7 @@ namespace lean {
 struct head_index {
     expr_kind m_kind;
     name      m_name;
-    explicit head_index(expr_kind k = expr_kind::Var):m_kind(k) {}
+    explicit head_index(expr_kind k = expr_kind::BVar):m_kind(k) {}
     explicit head_index(name const & c):m_kind(expr_kind::Constant), m_name(c) {}
     head_index(expr const & e);
     expr_kind kind() const { return m_kind; }
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 4876e3dee2..a88d1b7bdc 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -581,7 +581,7 @@ class add_nested_inductive_decl_fn {
         expr e = safe_whnf(m_tctx, _e);
         switch (e.kind()) {
         case expr_kind::Sort:
-        case expr_kind::Local:
+        case expr_kind::FVar:
         case expr_kind::Macro:
             return _e;
         case expr_kind::Lambda:
@@ -620,7 +620,7 @@ class add_nested_inductive_decl_fn {
             }
             return _e;
         }
-        case expr_kind::Var:
+        case expr_kind::BVar:
         case expr_kind::Meta:
         case expr_kind::Let:
             lean_unreachable();
@@ -635,7 +635,7 @@ class add_nested_inductive_decl_fn {
         expr e = safe_whnf(m_tctx, _e);
         switch (e.kind()) {
         case expr_kind::Sort:
-        case expr_kind::Local:
+        case expr_kind::FVar:
         case expr_kind::Macro:
             return _e;
         case expr_kind::Lambda:
@@ -674,7 +674,7 @@ class add_nested_inductive_decl_fn {
             }
             return _e;
         }
-        case expr_kind::Var:
+        case expr_kind::BVar:
         case expr_kind::Meta:
         case expr_kind::Let:
             lean_unreachable();
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 3c89fdb8c3..7b8aec3585 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -74,7 +74,7 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
         super::write_core(a, static_cast<char>(k), [&]() {
                 serializer & s = get_owner();
                 switch (k) {
-                case expr_kind::Var:
+                case expr_kind::BVar:
                     s << var_idx(a);
                     break;
                 case expr_kind::Constant:
@@ -107,7 +107,7 @@ class expr_serializer : public object_serializer<expr, expr_hash, is_bi_equal_pr
                     lean_assert(!mlocal_name(a).is_anonymous());
                     s << mlocal_name(a) << mlocal_pp_name(a); write_core(mlocal_type(a));
                     break;
-                case expr_kind::Local:
+                case expr_kind::FVar:
                     lean_assert(!mlocal_name(a).is_anonymous());
                     lean_assert(!mlocal_pp_name(a).is_anonymous());
                     s << mlocal_name(a) << mlocal_pp_name(a) << local_info(a); write_core(mlocal_type(a));
@@ -138,7 +138,7 @@ public:
                 deserializer & d = get_owner();
                 auto k = static_cast<expr_kind>(c);
                 switch (k) {
-                case expr_kind::Var:
+                case expr_kind::BVar:
                     return mk_var(d.read_unsigned());
                 case expr_kind::Constant: {
                     auto n = read_name(d);
@@ -171,7 +171,7 @@ public:
                     name pp_n = read_name(d);
                     return mk_metavar(n, pp_n, read());
                 }
-                case expr_kind::Local: {
+                case expr_kind::FVar: {
                     name n         = read_name(d);
                     name pp_n      = read_name(d);
                     binder_info bi = read_binder_info(d);
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index 659d4570d5..e238aa1496 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -72,9 +72,9 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
             return;
         visited.insert(e);
         switch (e.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort:
+        case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
             break; // do nothing
-        case expr_kind::Local:
+        case expr_kind::FVar:
             if (!restricted)
                 visit(mlocal_type(e));
             ls.insert(e);
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 0fb07a5731..6c57deb400 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -53,7 +53,7 @@ struct max_sharing_fn::imp {
             return *r;
         expr res;
         switch (a.kind()) {
-        case expr_kind::Var:
+        case expr_kind::BVar:
             res = a;
             break;
         case expr_kind::Constant:
@@ -81,7 +81,7 @@ struct max_sharing_fn::imp {
             res = update_let(a, new_t, new_v, new_b);
             break;
         }
-        case expr_kind::Meta:  case expr_kind::Local:
+        case expr_kind::Meta:  case expr_kind::FVar:
             res = update_mlocal(a, apply(mlocal_type(a)));
             break;
         case expr_kind::Macro: {
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 862d478f1c..4fef23da17 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -192,9 +192,9 @@ struct get_noncomputable_reason_fn {
         case expr_kind::Sort:      return;
         case expr_kind::Macro:     visit_macro(e);    return;
         case expr_kind::Constant:  visit_constant(e); return;
-        case expr_kind::Var:       lean_unreachable();
+        case expr_kind::BVar:      lean_unreachable();
         case expr_kind::Meta:      lean_unreachable();
-        case expr_kind::Local:     return;
+        case expr_kind::FVar:      return;
         case expr_kind::App:       visit_app(e);      return;
         case expr_kind::Lambda:    visit_binding(e);  return;
         case expr_kind::Pi:        visit_binding(e);  return;
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 5b0d47ba74..a05cdbda94 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -116,8 +116,8 @@ class normalize_fn {
             return e;
         e = m_ctx.whnf(e);
         switch (e.kind()) {
-        case expr_kind::Var:  case expr_kind::Constant: case expr_kind::Sort:
-        case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro:
+        case expr_kind::BVar: case expr_kind::Constant: case expr_kind::Sort:
+        case expr_kind::Meta: case expr_kind::FVar: case expr_kind::Macro:
             return e;
         case expr_kind::Lambda: {
             e = normalize_binding(e);
diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp
index 7dcd0b11cc..b501410288 100644
--- a/src/library/pos_info_provider.cpp
+++ b/src/library/pos_info_provider.cpp
@@ -136,9 +136,9 @@ class replace_rec_fn2 {
             return save_result(e, offset, *r, shared);
         } else {
             switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Var:
+            case expr_kind::Constant: case expr_kind::Sort: case expr_kind::BVar:
                 return save_result(e, offset, e, shared);
-            case expr_kind::Meta:     case expr_kind::Local: {
+            case expr_kind::Meta:     case expr_kind::FVar: {
                 expr new_t = apply(mlocal_type(e), offset);
                 return save_result(e, offset, copy_pos(e, update_mlocal(e, new_t)), shared);
             }
diff --git a/src/library/print.cpp b/src/library/print.cpp
index 6f42ec64c6..b78b7c5179 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -218,10 +218,10 @@ struct print_expr_fn {
         case expr_kind::Meta:
             out() << "?" << fix_name(mlocal_name(a));
             break;
-        case expr_kind::Local:
+        case expr_kind::FVar:
             out() << fix_name(mlocal_pp_name(a));
             break;
-        case expr_kind::Var:
+        case expr_kind::BVar:
             out() << "#" << var_idx(a);
             break;
         case expr_kind::Constant:
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index be25c8492c..df1d48f4d5 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -69,9 +69,9 @@ expr replace_visitor::visit(expr const & e) {
     case expr_kind::Sort:      return save_result(e, visit_sort(e), shared);
     case expr_kind::Macro:     return save_result(e, visit_macro(e), shared);
     case expr_kind::Constant:  return save_result(e, visit_constant(e), shared);
-    case expr_kind::Var:       return save_result(e, visit_var(e), shared);
+    case expr_kind::BVar:      return save_result(e, visit_var(e), shared);
     case expr_kind::Meta:      return save_result(e, visit_meta(e), shared);
-    case expr_kind::Local:     return save_result(e, visit_local(e), shared);
+    case expr_kind::FVar:      return save_result(e, visit_local(e), shared);
     case expr_kind::App:       return save_result(e, visit_app(e), shared);
     case expr_kind::Lambda:    return save_result(e, visit_lambda(e), shared);
     case expr_kind::Pi:        return save_result(e, visit_pi(e), shared);
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index f801142b19..b248bf4766 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -254,12 +254,12 @@ expr dsimplify_core_fn::visit(expr const & e) {
     while (true) {
         expr new_e;
         switch (curr_e.kind()) {
-        case expr_kind::Local:
+        case expr_kind::FVar:
         case expr_kind::Sort:
         case expr_kind::Constant:
             new_e = curr_e;
             break;
-        case expr_kind::Var:
+        case expr_kind::BVar:
             lean_unreachable();
         case expr_kind::Meta:
             new_e = visit_meta(curr_e);
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index f160e38257..c6a93a2462 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -630,9 +630,9 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
         return false;
     switch (lhs.kind()) {
     case expr_kind::Constant: case expr_kind::Sort:
-    case expr_kind::Meta: case expr_kind::Local:
+    case expr_kind::Meta: case expr_kind::FVar:
         return lhs == rhs;
-    case expr_kind::Var:
+    case expr_kind::BVar:
         if (var_idx(lhs) < offset) {
             return lhs == rhs; // locally bound variable
         } else if (var_idx(lhs) - offset < p.size()) {
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index ccf48294a2..46aa8b8558 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -644,7 +644,7 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
     while (true) {
         simp_result new_result;
         switch (curr_result.get_new().kind()) {
-        case expr_kind::Local:
+        case expr_kind::FVar:
         case expr_kind::Sort:
         case expr_kind::Constant:
             new_result = curr_result;
@@ -656,7 +656,7 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         case expr_kind::Macro:
             new_result = join(curr_result, visit_macro(curr_result.get_new()));
             break;
-        case expr_kind::Var:
+        case expr_kind::BVar:
             lean_unreachable();
         case expr_kind::Lambda:
             new_result = join(curr_result, visit_lambda(curr_result.get_new()));
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 24f82ac3c8..4c2d233bac 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -785,12 +785,12 @@ optional<expr> type_context_old::reduce_recursor(expr const & e) {
 expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
     expr e = e0;
     while (true) { switch (e.kind()) {
-    case expr_kind::Var:      case expr_kind::Sort:
+    case expr_kind::BVar:     case expr_kind::Sort:
     case expr_kind::Pi:       case expr_kind::Lambda:
     case expr_kind::Constant:
         /* Remark: we do not unfold Constants eagerly in this method */
         return e;
-    case expr_kind::Local:
+    case expr_kind::FVar:
         if (use_zeta() && is_local_decl_ref(e)) {
             if (auto d = m_lctx.find_local_decl(e)) {
                 if (auto v = d->get_value()) {
@@ -887,7 +887,7 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
 
 expr type_context_old::whnf(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var:      case expr_kind::Sort:
+    case expr_kind::BVar:     case expr_kind::Sort:
     case expr_kind::Pi:       case expr_kind::Lambda:
         return e;
     default:
@@ -997,13 +997,13 @@ expr type_context_old::infer_core(expr const & e) {
 
     expr r;
     switch (e.kind()) {
-    case expr_kind::Local:
+    case expr_kind::FVar:
         r = infer_local(e);
         break;
     case expr_kind::Meta:
         r = infer_metavar(e);
         break;
-    case expr_kind::Var:
+    case expr_kind::BVar:
         throw exception("failed to infer type, unexpected bound variable occurrence");
     case expr_kind::Sort:
         r = mk_sort(mk_succ(sort_level(e)));
@@ -2702,8 +2702,8 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
             return to_lbool(is_def_eq_binding(e1, e2));
         case expr_kind::Sort:
             return to_lbool(is_def_eq(sort_level(e1), sort_level(e2)));
-        case expr_kind::Meta:     case expr_kind::Var:
-        case expr_kind::Local:    case expr_kind::App:
+        case expr_kind::Meta:     case expr_kind::BVar:
+        case expr_kind::FVar:     case expr_kind::App:
         case expr_kind::Constant: case expr_kind::Macro:
         case expr_kind::Let:
             // We do not handle these cases in this method.
@@ -3321,7 +3321,7 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
     expr const * it = &type;
     while (true) {
         switch (it->kind()) {
-        case expr_kind::Var:  case expr_kind::Sort:   case expr_kind::Local:
+        case expr_kind::BVar: case expr_kind::Sort:   case expr_kind::FVar:
         case expr_kind::Meta: case expr_kind::Lambda:
             return l_false;
         case expr_kind::Let:
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index df0b7f7d14..706f3d3936 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -161,7 +161,7 @@ vm_obj expr_macro_def_name(vm_obj const & d) {
 unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
     expr const & e = to_expr(o);
     switch (e.kind()) {
-    case expr_kind::Var:
+    case expr_kind::BVar:
         data.push_back(mk_vm_nat(var_idx(e)));
         break;
     case expr_kind::Sort:
@@ -176,7 +176,7 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
         data.push_back(to_obj(mlocal_pp_name(e)));
         data.push_back(to_obj(mlocal_type(e)));
         break;
-    case expr_kind::Local:
+    case expr_kind::FVar:
         data.push_back(to_obj(mlocal_name(e)));
         break;
     case expr_kind::App: