diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 1cd2db739..72bf55ab7 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -74,11 +74,11 @@ expr app(unsigned n, expr const * as) {
     return r;
 }
 
-expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e):
-    expr_cell(k, ::lean::hash(t.hash(), e.hash())),
+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_expr(e) {
+    m_body(b) {
 }
 expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
     expr_abstraction(expr_kind::Lambda, n, t, e) {}
@@ -147,7 +147,7 @@ public:
         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_expr(a), abst_expr(b));
+            return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
         case expr_kind::Prop:     lean_unreachable(); return true;
         case expr_kind::Type:
             if (ty_num_vars(a) != ty_num_vars(b))
@@ -184,8 +184,8 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
         }
         out << ")";
         break;
-    case expr_kind::Lambda:  out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")";    break;
-    case expr_kind::Pi:      out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")"; break;
+    case expr_kind::Lambda:  out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")";    break;
+    case expr_kind::Pi:      out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
     case expr_kind::Prop:    out << "Prop"; break;
     case expr_kind::Type:    out << "Type"; break;
     case expr_kind::Numeral: out << num_value(a); break;
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index a149802a2..8374113f9 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -172,12 +172,12 @@ public:
 class expr_abstraction : public expr_cell {
     name     m_name;
     expr     m_type;
-    expr     m_expr;
+    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_expr() const { return m_expr; }
+    expr const & get_body() const { return m_body; }
 };
 // 5. Lambda
 class expr_lambda : public expr_abstraction {
@@ -299,7 +299,7 @@ inline unsigned     num_args(expr_cell * e)             { return to_app(e)->get_
 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_expr(expr_cell * e)            { return to_abstraction(e)->get_expr(); }
+inline expr const & abst_body(expr_cell * e)            { return to_abstraction(e)->get_body(); }
 inline unsigned     ty_num_vars(expr_cell * e)          { return to_type(e)->size(); }
 inline uvar const & ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); }
 inline mpz const &  num_value(expr_cell * e)            { return to_numeral(e)->get_num(); }
@@ -315,7 +315,7 @@ inline expr const * begin_args(expr const & e)           { return to_app(e)->beg
 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_expr(expr const & e)            { return to_abstraction(e)->get_expr(); }
+inline expr const & abst_body(expr const & e)            { return to_abstraction(e)->get_body(); }
 inline unsigned     ty_num_vars(expr const & e)          { return to_type(e)->size(); }
 inline uvar const & ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); }
 inline mpz const &  num_value(expr const & e)            { return to_numeral(e)->get_num(); }
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index f191ef3dc..2b9913a40 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -45,7 +45,7 @@ public:
             break;
         case expr_kind::Lambda:
         case expr_kind::Pi:
-            result = apply(abst_type(e), offset) || apply(abst_expr(e), offset + 1);
+            result = apply(abst_type(e), offset) || apply(abst_body(e), offset + 1);
             break;
         }
 
diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp
index 6aee9179b..9f5c519bb 100644
--- a/src/kernel/max_sharing.cpp
+++ b/src/kernel/max_sharing.cpp
@@ -58,12 +58,12 @@ public:
         case expr_kind::Lambda:
         case expr_kind::Pi: {
             expr const & old_t = abst_type(a);
-            expr const & old_e = abst_expr(a);
+            expr const & old_b = abst_body(a);
             expr t = apply(old_t);
-            expr e = apply(old_e);
-            if (!eqp(t, old_t) || !eqp(e, old_e)) {
+            expr b = apply(old_b);
+            if (!eqp(t, old_t) || !eqp(b, old_b)) {
                 name const & n     = abst_name(a);
-                expr r = is_pi(a) ? pi(n, t, e) : lambda(n, t, e);
+                expr r = is_pi(a) ? pi(n, t, b) : lambda(n, t, b);
                 cache(r);
                 return r;
             }
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 7f55c776c..2fcef6b4b 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -53,7 +53,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_expr(e))) + 1;
+        return std::max(depth1(abst_type(e)), depth1(abst_body(e))) + 1;
     }
     return 0;
 }
@@ -69,7 +69,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_expr(e))) + 1;
+        return std::max(depth2(abst_type(e)), depth2(abst_body(e))) + 1;
     }
     return 0;
 }
@@ -96,7 +96,7 @@ unsigned depth3(expr const & e) {
         }
         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_expr(e), c));
+            todo.push_back(std::make_pair(&abst_body(e), c));
             break;
         }
     }
@@ -152,7 +152,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_expr(a), s) + 1;
+        return count_core(abst_type(a), s) + count_core(abst_body(a), s) + 1;
     }
     return 0;
 }