diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh
index 4098c7ac10..f07487332e 100644
--- a/script/prepare-llvm-mingw.sh
+++ b/script/prepare-llvm-mingw.sh
@@ -50,5 +50,4 @@ echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic
 # when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests
-echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
 echo -n " -DLEAN_TEST_VARS=''"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0457c08dee..7dcb366bc6 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -58,9 +58,6 @@ option(USE_GITHASH        "GIT_HASH"           ON)
 option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
 # When ON we install a copy of cadical
 option(INSTALL_CADICAL "Install a copy of cadical" ON)
-# When ON thread storage is automatically finalized, it assumes platform support pthreads.
-# This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell).
-option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON)
 
 # FLAGS for disabling optimizations and debugging
 option(FREE_VAR_RANGE_OPT  "FREE_VAR_RANGE_OPT"   ON)
@@ -182,10 +179,6 @@ else()
   string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_MULTI_THREAD")
 endif()
 
-if(AUTO_THREAD_FINALIZATION AND NOT MSVC)
-  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_AUTO_THREAD_FINALIZATION")
-endif()
-
 # Set Module Path
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp
index cd53bae6ad..7df3d8f2f7 100644
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -9,9 +9,6 @@ Author: Leonardo de Moura
 #include <iostream>
 #ifdef LEAN_WINDOWS
 #include <windows.h>
-# ifdef LEAN_AUTO_THREAD_FINALIZATION
-#include <pthread.h>
-# endif
 #else
 #include <pthread.h>
 #endif
@@ -179,107 +176,6 @@ void run_thread_finalizers_core(thread_finalizers & fns) {
     fns.clear();
 }
 
-// We have two different implementations of the following procedures.
-//
-//   void register_thread_finalizer(thread_finalizer fn, void * p);
-//   void register_post_thread_finalizer(thread_finalizer fn, void * p);
-//   void run_thread_finalizers();
-//
-// The implementation is selected by using the LEAN_AUTO_THREAD_FINALIZATION compilation directive.
-// We can remove the implementation based on pthreads after the new thread_local C++11 keyword is properly
-// implemented in all platforms.
-// In the meantime, when LEAN_AUTO_THREAD_FINALIZATION is defined/set, we use a thread finalization
-// procedure based on the pthread API.
-// Remark: we only need this feature when Lean is being used as a library.
-// Example: the C API is being used from Haskell, and the execution threads
-// are being created by Haskell.
-// Remark: for the threads created by Lean, we explicitly create the thread finalizers.
-// The idea is to avoid memory leaks even when LEAN_AUTO_THREAD_FINALIZATION is not used.
-
-#if defined(LEAN_AUTO_THREAD_FINALIZATION)
-// pthread based implementation
-
-typedef std::pair<thread_finalizers, thread_finalizers> thread_finalizers_pair;
-
-class thread_finalizers_manager {
-    pthread_key_t g_key;
-public:
-    thread_finalizers_manager() {
-        pthread_key_create(&g_key, finalize_thread);
-        init_thread(); // initialize main thread
-    }
-
-    ~thread_finalizers_manager() {
-        finalize_thread(get_pair()); // finalize main thread
-        pthread_key_delete(g_key);
-    }
-
-    thread_finalizers_pair * get_pair() {
-        return reinterpret_cast<thread_finalizers_pair*>(pthread_getspecific(g_key));
-    }
-
-    void init_thread() {
-        if (get_pair() == nullptr) {
-            thread_finalizers_pair * p = new thread_finalizers_pair();
-            pthread_setspecific(g_key, p);
-        }
-    }
-
-    thread_finalizers & get_thread_finalizers() {
-        init_thread();
-        return get_pair()->first;
-    }
-
-    thread_finalizers & get_post_thread_finalizers() {
-        init_thread();
-        return get_pair()->second;
-    }
-
-    static void finalize_thread(void * d) {
-        if (d) {
-            thread_finalizers_pair * p = reinterpret_cast<thread_finalizers_pair*>(d);
-            run_thread_finalizers_core(p->first);
-            run_thread_finalizers_core(p->second);
-            delete p;
-        }
-    }
-};
-
-static thread_finalizers_manager * g_thread_finalizers_mgr = nullptr;
-
-// TODO(gabriel): race condition with thread finalizers
-void delete_thread_finalizer_manager() {
-    // delete g_thread_finalizers_mgr;
-    // g_thread_finalizers_mgr = nullptr;
-}
-
-void register_thread_finalizer(thread_finalizer fn, void * p) {
-    g_thread_finalizers_mgr->get_thread_finalizers().emplace_back(fn, p);
-}
-
-void register_post_thread_finalizer(thread_finalizer fn, void * p) {
-    g_thread_finalizers_mgr->get_post_thread_finalizers().emplace_back(fn, p);
-}
-
-void run_thread_finalizers() {
-    if (auto p = g_thread_finalizers_mgr->get_pair())
-        run_thread_finalizers_core(p->first);
-}
-
-void run_post_thread_finalizers() {
-    if (auto p = g_thread_finalizers_mgr->get_pair())
-        run_thread_finalizers_core(p->second);
-}
-
-void initialize_thread() {
-    g_thread_finalizers_mgr = new thread_finalizers_manager;
-    initialize_thread_local_reset_fns();
-}
-void finalize_thread() {
-    finalize_thread_local_reset_fns();
-}
-#else
-// reference implementation
 LEAN_THREAD_PTR(thread_finalizers, g_finalizers);
 LEAN_THREAD_PTR(thread_finalizers, g_post_finalizers);
 
@@ -320,5 +216,4 @@ void initialize_thread() {
 void finalize_thread() {
     finalize_thread_local_reset_fns();
 }
-#endif
 }