diff --git a/stage0/src/include/lean/lean.h b/stage0/src/include/lean/lean.h
index 60a7b43c9c..1bbbe7b774 100644
--- a/stage0/src/include/lean/lean.h
+++ b/stage0/src/include/lean/lean.h
@@ -698,11 +698,6 @@ static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, uns
     return o;
 }
 
-// TODO: delete
-static inline lean_object * lean_alloc_ctor_big(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
-    return lean_alloc_ctor(tag, num_objs, scalar_sz);
-}
-
 static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) {
     assert(i < lean_ctor_num_objs(o));
     return lean_ctor_obj_cptr(o)[i];
diff --git a/stage0/src/include/lean/object.h b/stage0/src/include/lean/object.h
index b634a401d9..2d77a7b4cf 100644
--- a/stage0/src/include/lean/object.h
+++ b/stage0/src/include/lean/object.h
@@ -79,7 +79,6 @@ inline unsigned cnstr_num_objs(object * o) { return lean_ctor_num_objs(o); }
 inline object ** cnstr_obj_cptr(object * o) { return lean_ctor_obj_cptr(o); }
 inline uint8 * cnstr_scalar_cptr(object * o) { return lean_ctor_scalar_cptr(o); }
 inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor(tag, num_objs, scalar_sz); }
-inline obj_res alloc_cnstr_big(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor_big(tag, num_objs, scalar_sz); }
 inline unsigned cnstr_tag(b_obj_arg o) { lean_assert(is_cnstr(o)); return lean_ptr_tag(o); }
 inline void cnstr_set_tag(b_obj_arg o, unsigned tag) { lean_ctor_set_tag(o, tag); }
 inline b_obj_res cnstr_get(b_obj_arg o, unsigned i) { return lean_ctor_get(o, i); }