diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 70179dd808..6231d4b219 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -29,6 +29,10 @@ void vm_obj_cell::dec_ref(vm_obj & o, buffer<vm_obj_cell*> & todelete) {
 
 MK_THREAD_LOCAL_GET(small_object_allocator, get_small_allocator, "vm object");
 
+small_object_allocator & get_vm_allocator() {
+    return get_small_allocator();
+}
+
 vm_composite::vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data):
     vm_obj_cell(k), m_idx(idx),  m_size(sz) {
     vm_obj * fields = get_field_ptr();
@@ -95,12 +99,6 @@ void vm_mpz::dealloc() {
     get_small_allocator().deallocate(sizeof(vm_mpz), this);
 }
 
-vm_obj mk_vm_external(vm_external * cell) {
-    lean_assert(cell);
-    lean_assert(cell->get_rc() == 0);
-    return vm_obj(cell);
-}
-
 void vm_obj_cell::dealloc() {
     try {
         buffer<vm_obj_cell*> todo;
@@ -114,7 +112,7 @@ void vm_obj_cell::dealloc() {
             case vm_obj_kind::Constructor: to_composite(it)->dealloc(todo); break;
             case vm_obj_kind::Closure:     to_composite(it)->dealloc(todo); break;
             case vm_obj_kind::MPZ:         to_mpz_core(it)->dealloc(); break;
-            case vm_obj_kind::External:    delete to_external(it); break;
+            case vm_obj_kind::External:    to_external(it)->dealloc(); break;
             }
         }
     } catch (std::bad_alloc&) {
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 4b80df77d3..8cfd792373 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/debug.h"
 #include "util/rc.h"
+#include "util/small_object_allocator.h"
 #include "util/serializer.h"
 #include "util/numerics/mpz.h"
 #include "kernel/environment.h"
@@ -123,11 +124,16 @@ public:
 };
 
 class vm_external : public vm_obj_cell {
+protected:
+    friend vm_obj_cell;
+    virtual void dealloc() = 0;
 public:
     vm_external():vm_obj_cell(vm_obj_kind::External) {}
-    virtual ~vm_external() {}
+    ~vm_external() {}
 };
 
+small_object_allocator & get_vm_allocator();
+
 // =======================================
 // Constructors
 vm_obj mk_vm_simple(unsigned cidx);
@@ -138,7 +144,7 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj c
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
 vm_obj mk_vm_mpz(mpz const & n);
-vm_obj mk_vm_external(vm_external * cell);
+inline vm_obj mk_vm_external(vm_external * obj) { lean_assert(obj && obj->get_rc() == 0); return vm_obj(obj); }
 /* helper functions for creating natural numbers */
 vm_obj mk_vm_nat(unsigned n);
 vm_obj mk_vm_nat(mpz const & n);
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 688320ace0..5e5aa530d0 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -24,7 +24,9 @@ namespace lean {
 struct vm_macro_definition : public vm_external {
     macro_definition m_val;
     vm_macro_definition(macro_definition const & v):m_val(v) {}
-    virtual ~vm_macro_definition() {}
+    virtual void dealloc() override {
+        this->~vm_macro_definition(); get_vm_allocator().deallocate(sizeof(vm_macro_definition), this);
+    }
 };
 
 macro_definition const & to_macro_definition(vm_obj const & o) {
@@ -34,13 +36,13 @@ macro_definition const & to_macro_definition(vm_obj const & o) {
 }
 
 vm_obj to_obj(macro_definition const & d) {
-    return mk_vm_external(new vm_macro_definition(d));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_macro_definition))) vm_macro_definition(d));
 }
 
 struct vm_expr : public vm_external {
     expr m_val;
     vm_expr(expr const & v):m_val(v) {}
-    virtual ~vm_expr() {}
+    virtual void dealloc() override { this->~vm_expr(); get_vm_allocator().deallocate(sizeof(vm_expr), this); }
 };
 
 expr const & to_expr(vm_obj const & o) {
@@ -50,7 +52,7 @@ expr const & to_expr(vm_obj const & o) {
 }
 
 vm_obj to_obj(expr const & e) {
-    return mk_vm_external(new vm_expr(e));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(e));
 }
 
 list<expr> to_list_expr(vm_obj const & o) {
diff --git a/src/library/vm/vm_format.cpp b/src/library/vm/vm_format.cpp
index ac6b1b857f..2d7f7d4f4c 100644
--- a/src/library/vm/vm_format.cpp
+++ b/src/library/vm/vm_format.cpp
@@ -15,7 +15,7 @@ namespace lean {
 struct vm_format : public vm_external {
     format m_val;
     vm_format(format const & v):m_val(v) {}
-    virtual ~vm_format() {}
+    virtual void dealloc() override { this->~vm_format(); get_vm_allocator().deallocate(sizeof(vm_format), this); }
 };
 
 format const & to_format(vm_obj const & o) {
@@ -25,7 +25,7 @@ format const & to_format(vm_obj const & o) {
 }
 
 vm_obj to_obj(format const & n) {
-    return mk_vm_external(new vm_format(n));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_format))) vm_format(n));
 }
 
 vm_obj format_line() {
diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp
index 147f91b5bb..e8836a9d95 100644
--- a/src/library/vm/vm_level.cpp
+++ b/src/library/vm/vm_level.cpp
@@ -17,7 +17,7 @@ namespace lean {
 struct vm_level : public vm_external {
     level m_val;
     vm_level(level const & v):m_val(v) {}
-    virtual ~vm_level() {}
+    virtual void dealloc() override { this->~vm_level(); get_vm_allocator().deallocate(sizeof(vm_level), this); }
 };
 
 level const & to_level(vm_obj const & o) {
@@ -27,7 +27,7 @@ level const & to_level(vm_obj const & o) {
 }
 
 vm_obj to_obj(level const & n) {
-    return mk_vm_external(new vm_level(n));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_level))) vm_level(n));
 }
 
 list<level> to_list_level(vm_obj const & o) {
diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp
index 225cb24d49..fa5b2c8d43 100644
--- a/src/library/vm/vm_name.cpp
+++ b/src/library/vm/vm_name.cpp
@@ -15,7 +15,7 @@ namespace lean {
 struct vm_name : public vm_external {
     name m_val;
     vm_name(name const & v):m_val(v) {}
-    virtual ~vm_name() {}
+    virtual void dealloc() override { this->~vm_name(); get_vm_allocator().deallocate(sizeof(vm_name), this); }
 };
 
 name const & to_name(vm_obj const & o) {
@@ -25,7 +25,7 @@ name const & to_name(vm_obj const & o) {
 }
 
 vm_obj to_obj(name const & n) {
-    return mk_vm_external(new vm_name(n));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_name))) vm_name(n));
 }
 
 list<name> to_list_name(vm_obj const & o) {
diff --git a/src/library/vm/vm_options.cpp b/src/library/vm/vm_options.cpp
index 2a9975e06a..9ef620c71b 100644
--- a/src/library/vm/vm_options.cpp
+++ b/src/library/vm/vm_options.cpp
@@ -15,7 +15,7 @@ namespace lean {
 struct vm_options : public vm_external {
     options m_val;
     vm_options(options const & v):m_val(v) {}
-    virtual ~vm_options() {}
+    virtual void dealloc() override { this->~vm_options(); get_vm_allocator().deallocate(sizeof(vm_options), this); }
 };
 
 options const & to_options(vm_obj const & o) {
@@ -25,7 +25,7 @@ options const & to_options(vm_obj const & o) {
 }
 
 vm_obj to_obj(options const & n) {
-    return mk_vm_external(new vm_options(n));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_options))) vm_options(n));
 }
 
 vm_obj options_size(vm_obj const & o) {
diff --git a/src/library/vm/vm_rb_map.cpp b/src/library/vm/vm_rb_map.cpp
index 6518fe6a6c..40c9fcbd84 100644
--- a/src/library/vm/vm_rb_map.cpp
+++ b/src/library/vm/vm_rb_map.cpp
@@ -26,7 +26,7 @@ typedef rb_map<vm_obj, vm_obj, vm_obj_cmp> vm_obj_map;
 struct vm_rb_map : public vm_external {
     vm_obj_map m_map;
     vm_rb_map(vm_obj_map const & m):m_map(m) {}
-    virtual ~vm_rb_map() {}
+    virtual void dealloc() override { this->~vm_rb_map(); get_vm_allocator().deallocate(sizeof(vm_rb_map), this); }
 };
 
 vm_obj_map const & to_map(vm_obj const & o) {
@@ -36,7 +36,7 @@ vm_obj_map const & to_map(vm_obj const & o) {
 }
 
 vm_obj to_obj(vm_rb_map const & n) {
-    return mk_vm_external(new vm_rb_map(n));
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(n));
 }
 
 vm_obj rb_map_mk_core(vm_obj const &, vm_obj const &, vm_obj const & cmp) {