diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index d796d3532..55da4762a 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -117,6 +117,10 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
 expr_local::expr_local(name const & n, name const & pp_name, expr const & t):
     expr_mlocal(false, n, t),
     m_pp_name(pp_name) {}
+void expr_local::dealloc(buffer<expr_cell*> & todelete) {
+    dec_ref(m_type, todelete);
+    delete(this);
+}
 
 // Composite expressions
 expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range):
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 831b3e72f..2e375bcf5 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -188,6 +188,7 @@ public:
 
 /** \brief Metavariables and local constants */
 class expr_mlocal : public expr_cell {
+protected:
     name   m_name;
     expr   m_type;
     friend expr_cell;
@@ -204,6 +205,8 @@ class expr_local : public expr_mlocal {
     // it is only used for pretty printing. This field is ignored
     // when comparing expressions.
     name m_pp_name;
+    friend expr_cell;
+    void dealloc(buffer<expr_cell*> & todelete);
 public:
     expr_local(name const & n, name const & pp_name, expr const & t);
     name const & get_pp_name() const { return m_pp_name; }