diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp
index 057c33ca8..32459dcd3 100644
--- a/src/kernel/deep_copy.cpp
+++ b/src/kernel/deep_copy.cpp
@@ -32,8 +32,8 @@ class deep_copy_fn {
             r = app(new_args.size(), new_args.data());
             break;
         }
-        case expr_kind::Lambda:   r = lambda(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
-        case expr_kind::Pi:       r = pi(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
+        case expr_kind::Lambda:   r = lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
+        case expr_kind::Pi:       r = pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
         }
         if (sh)
             m_cache.insert(std::make_pair(a.raw(), r));
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index c4ff8c221..d3c35d707 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -76,7 +76,7 @@ expr app(unsigned n, expr const * as) {
 expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b):
     expr_cell(k, ::lean::hash(t.hash(), b.hash())),
     m_name(n),
-    m_type(t),
+    m_domain(t),
     m_body(b) {
 }
 expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
@@ -134,7 +134,7 @@ class eq_fn {
         case expr_kind::Pi:
             // Lambda and Pi
             // Remark: we ignore get_abs_name because we want alpha-equivalence
-            return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
+            return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
         case expr_kind::Type:     return ty_level(a) == ty_level(b);
         case expr_kind::Numeral:  return num_value(a) == num_value(b);
         }
@@ -168,14 +168,14 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
         }
         out << ")";
         break;
-    case expr_kind::Lambda:  out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")";    break;
+    case expr_kind::Lambda:  out << "(fun (" << abst_name(a) << " : " << abst_domain(a) << ") " << abst_body(a) << ")";    break;
     case expr_kind::Pi:
         if (!is_arrow(a))
-            out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")";
-        else if (!is_arrow(abst_type(a)))
-            out << abst_type(a) << " -> " << abst_body(a);
+            out << "(pi (" << abst_name(a) << " : " << abst_domain(a) << ") " << abst_body(a) << ")";
+        else if (!is_arrow(abst_domain(a)))
+            out << abst_domain(a) << " -> " << abst_body(a);
         else
-            out << "(" << abst_type(a) << ") -> " << abst_body(a);
+            out << "(" << abst_domain(a) << ") -> " << abst_body(a);
         break;
     case expr_kind::Type: {
         level const & l = ty_level(a);
@@ -197,8 +197,8 @@ expr copy(expr const & a) {
     case expr_kind::Type:     return type(ty_level(a));
     case expr_kind::Numeral:  return numeral(num_value(a));
     case expr_kind::App:      return app(num_args(a), begin_args(a));
-    case expr_kind::Lambda:   return lambda(abst_name(a), abst_type(a), abst_body(a));
-    case expr_kind::Pi:       return pi(abst_name(a), abst_type(a), abst_body(a));
+    case expr_kind::Lambda:   return lambda(abst_name(a), abst_domain(a), abst_body(a));
+    case expr_kind::Pi:       return pi(abst_name(a), abst_domain(a), abst_body(a));
     }
     lean_unreachable();
     return expr();
@@ -227,7 +227,7 @@ lean::format pp_aux(lean::expr const & a) {
                        paren(format{
                                format(abst_name(a)),
                                format(" : "),
-                               pp_aux(abst_type(a))}),
+                               pp_aux(abst_domain(a))}),
                        format(" "),
                        pp_aux(abst_body(a))});
     case expr_kind::Pi:
@@ -236,7 +236,7 @@ lean::format pp_aux(lean::expr const & a) {
                        paren(format{
                                format(abst_name(a)),
                                format(" : "),
-                               pp_aux(abst_type(a))}),
+                               pp_aux(abst_domain(a))}),
                        format(" "),
                        pp_aux(abst_body(a))});
     case expr_kind::Type:
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 6e7ca517d..2fe847d76 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -71,7 +71,7 @@ private:
     expr_cell * m_ptr;
     explicit expr(expr_cell * ptr):m_ptr(ptr) {}
 public:
-    expr():m_ptr(0) {}
+    expr():m_ptr(nullptr) {}
     expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~expr() { if (m_ptr) m_ptr->dec_ref(); }
@@ -144,13 +144,13 @@ public:
 /** \brief Super class for lambda abstraction and pi (functional spaces). */
 class expr_abstraction : public expr_cell {
     name     m_name;
-    expr     m_type;
+    expr     m_domain;
     expr     m_body;
 public:
     expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e);
-    name const & get_name() const { return m_name; }
-    expr const & get_type() const { return m_type; }
-    expr const & get_body() const { return m_body; }
+    name const & get_name() const   { return m_name; }
+    expr const & get_domain() const { return m_domain; }
+    expr const & get_body() const   { return m_body; }
 };
 /** \brief Lambda abstractions */
 class expr_lambda : public expr_abstraction {
@@ -258,7 +258,7 @@ inline unsigned      const_pos(expr_cell * e)            { return to_constant(e)
 inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
 inline name const &  abst_name(expr_cell * e)            { return to_abstraction(e)->get_name(); }
-inline expr const &  abst_type(expr_cell * e)            { return to_abstraction(e)->get_type(); }
+inline expr const &  abst_domain(expr_cell * e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr_cell * e)            { return to_abstraction(e)->get_body(); }
 inline level const & ty_level(expr_cell * e)             { return to_type(e)->get_level(); }
 inline mpz const &   num_value(expr_cell * e)            { return to_numeral(e)->get_num(); }
@@ -274,7 +274,7 @@ inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->ge
 inline expr const *  begin_args(expr const & e)           { return to_app(e)->begin_args(); }
 inline expr const *  end_args(expr const & e)             { return to_app(e)->end_args(); }
 inline name const &  abst_name(expr const & e)            { return to_abstraction(e)->get_name(); }
-inline expr const &  abst_type(expr const & e)            { return to_abstraction(e)->get_type(); }
+inline expr const &  abst_domain(expr const & e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr const & e)            { return to_abstraction(e)->get_body(); }
 inline level const & ty_level(expr const & e)             { return to_type(e)->get_level(); }
 inline mpz const &   num_value(expr const & e)            { return to_numeral(e)->get_num(); }
@@ -357,7 +357,7 @@ template<typename F> expr update_app(expr const & e, F f) {
 }
 template<typename F> expr update_abst(expr const & e, F f) {
     static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
-                               std::pair<expr, expr>>::value,
+                  std::pair<expr, expr>>::value,
                   "update_abst: return type of f is not pair<expr, expr>");
     expr const & old_t = abst_type(e);
     expr const & old_b = abst_body(e);
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index 54d57e8c1..b0d11b988 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -52,7 +52,7 @@ protected:
             break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
-            result = apply(abst_type(e), offset) || apply(abst_body(e), offset + 1);
+            result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
             break;
         }
 
diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index fc8badfa7..5fed10648 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -74,7 +74,7 @@ class normalize_fn {
 
     expr reify_closure(expr const & a, stack const & c, unsigned k) {
         lean_assert(is_lambda(a));
-        expr new_t = reify(normalize(abst_type(a), c, k), k);
+        expr new_t = reify(normalize(abst_domain(a), c, k), k);
         expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
         return lambda(abst_name(a), new_t, new_b);
 #if 0
@@ -156,7 +156,7 @@ class normalize_fn {
         case expr_kind::Lambda:
             return value(a, c);
         case expr_kind::Pi: {
-            expr new_t = reify(normalize(abst_type(a), c, k), k);
+            expr new_t = reify(normalize(abst_domain(a), c, k), k);
             expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
             return value(pi(abst_name(a), new_t, new_b));
         }}
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index 49774224b..5e2fbb498 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -90,7 +90,7 @@ class infer_type_fn {
             while (true) {
                 expr const & c = arg(e, i);
                 expr c_t       = infer_type(c, ctx);
-                check_type(e, i, abst_type(f_t), c_t, ctx);
+                check_type(e, i, abst_domain(f_t), c_t, ctx);
                 // Remark: if f_t is an arrow, we don't have to call normalize and
                 // lower_free_vars
                 f_t = normalize(abst_body(f_t), ctx, c);
@@ -103,13 +103,13 @@ class infer_type_fn {
             }
         }
         case expr_kind::Lambda: {
-            infer_universe(abst_type(e), ctx);
-            expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
-            return pi(abst_name(e), abst_type(e), t);
+            infer_universe(abst_domain(e), ctx);
+            expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
+            return pi(abst_name(e), abst_domain(e), t);
         }
         case expr_kind::Pi: {
-            level l1 = infer_universe(abst_type(e), ctx);
-            level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
+            level l1 = infer_universe(abst_domain(e), ctx);
+            level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
             return type(max(l1, l2));
         }
         case expr_kind::Numeral:
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 1267e1354..845be36e5 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -75,7 +75,7 @@ unsigned depth1(expr const & e) {
         return m + 1;
     }
     case expr_kind::Lambda: case expr_kind::Pi:
-        return std::max(depth1(abst_type(e)), depth1(abst_body(e))) + 1;
+        return std::max(depth1(abst_domain(e)), depth1(abst_body(e))) + 1;
     }
     return 0;
 }
@@ -91,7 +91,7 @@ unsigned depth2(expr const & e) {
                             [](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
             + 1;
     case expr_kind::Lambda: case expr_kind::Pi:
-        return std::max(depth2(abst_type(e)), depth2(abst_body(e))) + 1;
+        return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1;
     }
     return 0;
 }
@@ -117,7 +117,7 @@ unsigned depth3(expr const & e) {
             break;
         }
         case expr_kind::Lambda: case expr_kind::Pi:
-            todo.push_back(std::make_pair(&abst_type(e), c));
+            todo.push_back(std::make_pair(&abst_domain(e), c));
             todo.push_back(std::make_pair(&abst_body(e), c));
             break;
         }
@@ -174,7 +174,7 @@ unsigned count_core(expr const & a, expr_set & s) {
         return std::accumulate(begin_args(a), end_args(a), 1,
                           [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
     case expr_kind::Lambda: case expr_kind::Pi:
-        return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
+        return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     }
     return 0;
 }
diff --git a/src/tests/kernel/normalize.cpp b/src/tests/kernel/normalize.cpp
index 2ddd93379..07f4c137d 100644
--- a/src/tests/kernel/normalize.cpp
+++ b/src/tests/kernel/normalize.cpp
@@ -63,7 +63,7 @@ unsigned count_core(expr const & a, expr_set & s) {
         return std::accumulate(begin_args(a), end_args(a), 1,
                                [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
     case expr_kind::Lambda: case expr_kind::Pi:
-        return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
+        return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
     }
     return 0;
 }