diff --git a/gen/apply.lean b/gen/apply.lean
index d9bf966245..51919b2560 100644
--- a/gen/apply.lean
+++ b/gen/apply.lean
@@ -74,7 +74,7 @@ do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n",
      emit "  default:\n",
        emit $ sformat! "    lean_assert(arity > {max});\n",
        emit $ sformat! "    obj * as[{n}] = {{ {args} };\n",
-       emit "    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
+       emit "    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
        emit "    for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
        emit $ sformat! "    for (unsigned i = 0; i < {n}; i++) args[fixed+i] = as[i];\n",
        emit "    obj * r = FNN(f)(args);\n",
@@ -84,7 +84,7 @@ do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n",
    emit $ sformat! "} else if (arity < fixed + {n}) {{\n",
      if n ≥ 2 then do
        emit $ sformat! "  obj * as[{n}] = {{ {args} };\n",
-       emit "  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
+       emit "  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
        emit "  for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
        emit "  for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n",
        emit "  obj * new_f = curry(f, arity, args);\n",
@@ -124,14 +124,14 @@ do emit "obj* apply_m(obj* f, unsigned n, obj** as) {\n",
    emit "unsigned arity = closure_arity(f);\n",
    emit "unsigned fixed = closure_num_fixed(f);\n",
    emit $ sformat! "if (arity == fixed + n) {{\n",
-     emit "  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
+     emit "  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
      emit "  for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
      emit "  for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];\n",
      emit "  obj * r = FNN(f)(args);\n",
      emit "  dec_ref(f);\n",
      emit "  return r;\n",
    emit $ sformat! "} else if (arity < fixed + n) {{\n",
-     emit "  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT\n",
+     emit "  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT\n",
      emit "  for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }\n",
      emit "  for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];\n",
      emit "  obj * new_f = FNN(f)(args);\n",
diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp
index d948bc4b0f..f2f111ebdf 100644
--- a/src/runtime/apply.cpp
+++ b/src/runtime/apply.cpp
@@ -141,7 +141,7 @@ if (arity == fixed + 1) {
   default:
     lean_assert(arity > 16);
     obj * as[1] = { a1 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 1; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -197,7 +197,7 @@ if (arity == fixed + 2) {
   default:
     lean_assert(arity > 16);
     obj * as[2] = { a1, a2 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 2; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -206,7 +206,7 @@ if (arity == fixed + 2) {
   }
 } else if (arity < fixed + 2) {
   obj * as[2] = { a1, a2 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -256,7 +256,7 @@ if (arity == fixed + 3) {
   default:
     lean_assert(arity > 16);
     obj * as[3] = { a1, a2, a3 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 3; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -265,7 +265,7 @@ if (arity == fixed + 3) {
   }
 } else if (arity < fixed + 3) {
   obj * as[3] = { a1, a2, a3 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -313,7 +313,7 @@ if (arity == fixed + 4) {
   default:
     lean_assert(arity > 16);
     obj * as[4] = { a1, a2, a3, a4 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 4; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -322,7 +322,7 @@ if (arity == fixed + 4) {
   }
 } else if (arity < fixed + 4) {
   obj * as[4] = { a1, a2, a3, a4 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -368,7 +368,7 @@ if (arity == fixed + 5) {
   default:
     lean_assert(arity > 16);
     obj * as[5] = { a1, a2, a3, a4, a5 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 5; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -377,7 +377,7 @@ if (arity == fixed + 5) {
   }
 } else if (arity < fixed + 5) {
   obj * as[5] = { a1, a2, a3, a4, a5 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -421,7 +421,7 @@ if (arity == fixed + 6) {
   default:
     lean_assert(arity > 16);
     obj * as[6] = { a1, a2, a3, a4, a5, a6 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 6; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -430,7 +430,7 @@ if (arity == fixed + 6) {
   }
 } else if (arity < fixed + 6) {
   obj * as[6] = { a1, a2, a3, a4, a5, a6 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -472,7 +472,7 @@ if (arity == fixed + 7) {
   default:
     lean_assert(arity > 16);
     obj * as[7] = { a1, a2, a3, a4, a5, a6, a7 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 7; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -481,7 +481,7 @@ if (arity == fixed + 7) {
   }
 } else if (arity < fixed + 7) {
   obj * as[7] = { a1, a2, a3, a4, a5, a6, a7 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -521,7 +521,7 @@ if (arity == fixed + 8) {
   default:
     lean_assert(arity > 16);
     obj * as[8] = { a1, a2, a3, a4, a5, a6, a7, a8 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 8; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -530,7 +530,7 @@ if (arity == fixed + 8) {
   }
 } else if (arity < fixed + 8) {
   obj * as[8] = { a1, a2, a3, a4, a5, a6, a7, a8 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -568,7 +568,7 @@ if (arity == fixed + 9) {
   default:
     lean_assert(arity > 16);
     obj * as[9] = { a1, a2, a3, a4, a5, a6, a7, a8, a9 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 9; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -577,7 +577,7 @@ if (arity == fixed + 9) {
   }
 } else if (arity < fixed + 9) {
   obj * as[9] = { a1, a2, a3, a4, a5, a6, a7, a8, a9 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -613,7 +613,7 @@ if (arity == fixed + 10) {
   default:
     lean_assert(arity > 16);
     obj * as[10] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 10; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -622,7 +622,7 @@ if (arity == fixed + 10) {
   }
 } else if (arity < fixed + 10) {
   obj * as[10] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -656,7 +656,7 @@ if (arity == fixed + 11) {
   default:
     lean_assert(arity > 16);
     obj * as[11] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 11; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -665,7 +665,7 @@ if (arity == fixed + 11) {
   }
 } else if (arity < fixed + 11) {
   obj * as[11] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -697,7 +697,7 @@ if (arity == fixed + 12) {
   default:
     lean_assert(arity > 16);
     obj * as[12] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 12; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -706,7 +706,7 @@ if (arity == fixed + 12) {
   }
 } else if (arity < fixed + 12) {
   obj * as[12] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -736,7 +736,7 @@ if (arity == fixed + 13) {
   default:
     lean_assert(arity > 16);
     obj * as[13] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 13; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -745,7 +745,7 @@ if (arity == fixed + 13) {
   }
 } else if (arity < fixed + 13) {
   obj * as[13] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -773,7 +773,7 @@ if (arity == fixed + 14) {
   default:
     lean_assert(arity > 16);
     obj * as[14] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 14; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -782,7 +782,7 @@ if (arity == fixed + 14) {
   }
 } else if (arity < fixed + 14) {
   obj * as[14] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -808,7 +808,7 @@ if (arity == fixed + 15) {
   default:
     lean_assert(arity > 16);
     obj * as[15] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 15; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -817,7 +817,7 @@ if (arity == fixed + 15) {
   }
 } else if (arity < fixed + 15) {
   obj * as[15] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -841,7 +841,7 @@ if (arity == fixed + 16) {
   default:
     lean_assert(arity > 16);
     obj * as[16] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16 };
-    obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
     for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
     for (unsigned i = 0; i < 16; i++) args[fixed+i] = as[i];
     obj * r = FNN(f)(args);
@@ -850,7 +850,7 @@ if (arity == fixed + 16) {
   }
 } else if (arity < fixed + 16) {
   obj * as[16] = { a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16 };
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = curry(f, arity, args);
@@ -865,14 +865,14 @@ lean_assert(n > 16);
 unsigned arity = closure_arity(f);
 unsigned fixed = closure_num_fixed(f);
 if (arity == fixed + n) {
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];
   obj * r = FNN(f)(args);
   dec_ref(f);
   return r;
 } else if (arity < fixed + n) {
-  obj ** args = static_cast<obj**>(lean::alloca(arity*sizeof(obj*))); // NOLINT
+  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
   for (unsigned i = 0; i < fixed; i++) { inc(fx(i)); args[i] = fx(i); }
   for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
   obj * new_f = FNN(f)(args);
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 01456bae24..7331da1f6b 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -16,6 +16,12 @@ Author: Leonardo de Moura
 #include "runtime/int64.h"
 #include "runtime/thread.h"
 
+#ifdef _MSC_VER
+#define LEAN_ALLOCA(s) ::_alloca(s)
+#else
+#define LEAN_ALLOCA(s) ::alloca(s)
+#endif
+
 namespace lean {
 typedef unsigned char      uint8;
 typedef unsigned short     uint16;
@@ -23,20 +29,6 @@ typedef unsigned           uint32;
 typedef unsigned long long uint64;
 typedef size_t             usize;
 
-/*
-The primitives implemented in the runtime do not modify the RC of its arguments.
-Callers are responsible for increasing/decreasing the RCs using the `inc`/`dec` operations.
-All new objects allocated by the primitives have RC == 1.
-*/
-
-inline void * alloca(size_t s) {
-#ifdef _MSC_VER
-    return ::_alloca(s);
-#else
-    return ::alloca(s);
-#endif
-}
-
 /* Objects can be stored in 5 different kinds of memory:
    - `MTHeap`: multi-threaded heap, the reference counter (RC) is updated using atomic operations.
       All objects reachable from an object in the `MTHeap` are in `MTHeap`, `Persistent` or `Region`.