diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index df3399953..489c4cd22 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "util/buffer.h"
 #include "util/object_serializer.h"
 #include "util/lru_cache.h"
-#include "util/fixed_size_allocator.h"
+#include "util/memory_pool.h"
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
 #include "kernel/free_vars.h"
@@ -94,7 +94,7 @@ bool is_meta(expr const & e) {
 }
 
 // Expr variables
-typedef fixed_size_allocator<sizeof(expr_var)> var_allocator;
+typedef memory_pool<sizeof(expr_var)> var_allocator;
 MK_THREAD_LOCAL_GET_DEF(var_allocator, get_var_allocator);
 expr_var::expr_var(unsigned idx):
     expr_cell(expr_kind::Var, idx, false, false, false, false),
@@ -108,7 +108,7 @@ void expr_var::dealloc() {
 }
 
 // Expr constants
-typedef fixed_size_allocator<sizeof(expr_const)> const_allocator;
+typedef memory_pool<sizeof(expr_const)> const_allocator;
 MK_THREAD_LOCAL_GET_DEF(const_allocator, get_const_allocator);
 expr_const::expr_const(name const & n, levels const & ls):
     expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)),
@@ -121,7 +121,7 @@ void expr_const::dealloc() {
 }
 
 // Expr metavariables and local variables
-typedef fixed_size_allocator<sizeof(expr_mlocal)> mlocal_allocator;
+typedef memory_pool<sizeof(expr_mlocal)> mlocal_allocator;
 MK_THREAD_LOCAL_GET_DEF(mlocal_allocator, get_mlocal_allocator);
 expr_mlocal::expr_mlocal(bool is_meta, name const & 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(),
@@ -135,7 +135,7 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
     get_mlocal_allocator().recyle(this);
 }
 
-typedef fixed_size_allocator<sizeof(expr_local)> local_allocator;
+typedef memory_pool<sizeof(expr_local)> local_allocator;
 MK_THREAD_LOCAL_GET_DEF(local_allocator, get_local_allocator);
 expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi):
     expr_mlocal(false, n, t),
@@ -155,7 +155,7 @@ expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool h
     m_free_var_range(fv_range) {}
 
 // Expr applications
-typedef fixed_size_allocator<sizeof(expr_app)> app_allocator;
+typedef memory_pool<sizeof(expr_app)> app_allocator;
 MK_THREAD_LOCAL_GET_DEF(app_allocator, get_app_allocator);
 expr_app::expr_app(expr const & fn, expr const & arg):
     expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()),
@@ -186,7 +186,7 @@ bool operator==(binder_info const & i1, binder_info const & i2) {
 }
 
 // Expr binders (Lambda, Pi)
-typedef fixed_size_allocator<sizeof(expr_binding)> binding_allocator;
+typedef memory_pool<sizeof(expr_binding)> binding_allocator;
 MK_THREAD_LOCAL_GET_DEF(binding_allocator, get_binding_allocator);
 expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i):
     expr_composite(k, ::lean::hash(t.hash(), b.hash()),
@@ -209,7 +209,7 @@ void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
 }
 
 // Expr Sort
-typedef fixed_size_allocator<sizeof(expr_sort)> sort_allocator;
+typedef memory_pool<sizeof(expr_sort)> sort_allocator;
 MK_THREAD_LOCAL_GET_DEF(sort_allocator, get_sort_allocator);
 expr_sort::expr_sort(level const & l):
     expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)),
diff --git a/src/util/fixed_size_allocator.h b/src/util/memory_pool.h
similarity index 83%
rename from src/util/fixed_size_allocator.h
rename to src/util/memory_pool.h
index fd29a3cbe..137ffb570 100644
--- a/src/util/fixed_size_allocator.h
+++ b/src/util/memory_pool.h
@@ -8,12 +8,13 @@ Author: Leonardo de Moura
 #include "util/memory.h"
 
 namespace lean {
+/** \brief Auxiliary object for "recycling" allocated memory of fixed size */
 template<unsigned Size>
-class fixed_size_allocator {
+class memory_pool {
     void * m_free_list;
 public:
-    fixed_size_allocator():m_free_list(nullptr) {}
-    ~fixed_size_allocator() {
+    memory_pool():m_free_list(nullptr) {}
+    ~memory_pool() {
         while (m_free_list != nullptr) {
             void * r = m_free_list;
             m_free_list = *(reinterpret_cast<void **>(r));