diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index ed9d44614d..2d66bc6c78 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -103,7 +103,6 @@ expr_app::expr_app(unsigned num_args, bool has_mv):
     expr_cell(expr_kind::App, 0, has_mv),
     m_num_args(num_args) {
 }
-expr_app::~expr_app() {}
 void expr_app::dealloc(buffer<expr_cell*> & todelete) {
     unsigned i = m_num_args;
     while (i > 0) {
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 49fc00971e..3ff294e49e 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -208,7 +208,6 @@ class expr_app : public expr_cell {
     void dealloc(buffer<expr_cell*> & todelete);
 public:
     expr_app(unsigned size, bool has_mv);
-    ~expr_app();
     unsigned     get_num_args() const        { return m_num_args; }
     expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; }
     expr const * begin_args() const          { return m_args; }