diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1c642adcd07b..2365d636a475 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -104,7 +104,6 @@ option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON)
 option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON)
 option(SAVE_INFO "SAVE_INFO" ON)
 option(MMAP "MMAP" ON)
-option(LAZY_RC "LAZY_RC" OFF)
 option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
@@ -139,10 +138,6 @@ if(WFAIL MATCHES "ON")
   string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 
-if(LAZY_RC MATCHES "ON")
-  set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
-endif()
-
 if(USE_MIMALLOC)
   set(LEAN_MIMALLOC "#define LEAN_MIMALLOC")
 endif()
diff --git a/src/config.h.in b/src/config.h.in
index a4d696ded384..cac4835e0f80 100644
--- a/src/config.h.in
+++ b/src/config.h.in
@@ -8,5 +8,4 @@ Author: Leonardo de Moura
 #include <lean/version.h>
 
 @LEAN_MIMALLOC@
-@LEAN_LAZY_RC@
 @LEAN_IS_STAGE0@
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 49213d7be079..9954c2c5d77d 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -345,19 +345,7 @@ static inline void dec(lean_object * o, lean_object* & todo) {
     }
 }
 
-#ifdef LEAN_LAZY_RC
-LEAN_THREAD_PTR(object, g_to_free);
-#endif
-
-static object * lean_del_core(object * o, object * todo);
-
 extern "C" LEAN_EXPORT lean_object * lean_alloc_object(size_t sz) {
-#ifdef LEAN_LAZY_RC
-     if (g_to_free) {
-         object * o = pop_back(g_to_free);
-         g_to_free = lean_del_core(o, g_to_free);
-     }
-#endif
 #ifdef LEAN_MIMALLOC
     void * r = mi_malloc(sz);
     if (r == nullptr) lean_internal_panic_out_of_memory();
@@ -473,9 +461,6 @@ extern "C" LEAN_EXPORT void lean_dec_ref_cold(lean_object * o) {
         if (std::atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, std::memory_order_acq_rel) != -1)
             return;
     }
-#ifdef LEAN_LAZY_RC
-    push_back(g_to_free, o);
-#else
     object * todo = nullptr;
     while (true) {
         todo = lean_del_core(o, todo);
@@ -483,7 +468,6 @@ extern "C" LEAN_EXPORT void lean_dec_ref_cold(lean_object * o) {
             return;
         o = pop_back(todo);
     }
-#endif
 }