diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index fad672f26d..3f54a776e4 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -315,17 +315,17 @@ expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * ar
                    g),
     m_definition(m),
     m_num_args(num) {
-    m_args = new expr[num];
-    for (unsigned i = 0; i < m_num_args; i++)
-        m_args[i] = args[i];
+    expr * data = get_args_ptr();
+    std::uninitialized_copy(args, args + num, data);
 }
 void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
-    for (unsigned i = 0; i < m_num_args; i++) dec_ref(m_args[i], todelete);
-    delete(this);
-}
-expr_macro::~expr_macro() {
-    delete[] m_args;
+    expr * args = get_args_ptr();
+    for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
+    this->~expr_macro();
+    char * mem = reinterpret_cast<char*>(this);
+    delete[] mem;
 }
+expr_macro::~expr_macro() {}
 
 // =======================================
 // Constructors
@@ -374,7 +374,8 @@ expr mk_constant(name const & n, levels const & ls, tag g) {
     return cache(expr(new (get_const_allocator().allocate()) expr_const(n, ls, g)));
 }
 expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g) {
-    return cache(expr(new expr_macro(m, num, args, g)));
+    char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
+    return cache(expr(new (mem) expr_macro(m, num, args, g)));
 }
 expr mk_metavar(name const & n, expr const & t, tag g) {
     return cache(expr(new (get_mlocal_allocator().allocate()) expr_mlocal(true, n, t, g)));
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index dc3f65b994..ba6f424420 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -389,18 +389,23 @@ public:
 class expr_macro : public expr_composite {
     macro_definition m_definition;
     unsigned         m_num_args;
-    expr *           m_args;
     friend class expr_cell;
     friend expr copy(expr const & a);
     friend expr update_macro(expr const & e, unsigned num, expr const * args);
     void dealloc(buffer<expr_cell*> & todelete);
+    expr * get_args_ptr() {
+        return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
+    }
+    expr const * get_args_ptr() const {
+        return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
+    }
 public:
     expr_macro(macro_definition const & v, unsigned num, expr const * args, tag g);
     ~expr_macro();
 
     macro_definition const & get_def() const { return m_definition; }
-    expr const * get_args() const { return m_args; }
-    expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; }
+    expr const * get_args() const { return get_args_ptr(); }
+    expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
     unsigned get_num_args() const { return m_num_args; }
 };