diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d1f3df49a..6f2256a96 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -93,6 +93,7 @@ if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
         message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.8 or greater.")
     endif ()
 elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__CLANG__")
   if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     # In OSX, clang requires "-stdlib=libc++" to support C++11
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++")
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index f38e3f7fe..5b932795b 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -14,6 +14,11 @@ Author: Leonardo de Moura
 #include "util/memory_pool.h"
 
 namespace lean {
+#if defined(__CLANG__) && defined(__APPLE__) && !defined(LEAN_USE_BOOST)
+    // TODO(Leo): remove when problen on clang++ OSX thread local storage implementation is fixed
+    #define LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE
+#endif
+
 /**
    \brief Left-leaning Red-Black Trees
 
@@ -63,6 +68,7 @@ class rb_tree : public CMP {
         node_cell(node_cell const & s):m_left(s.m_left), m_right(s.m_right), m_value(s.m_value), m_red(s.m_red), m_rc(0) {}
     };
 
+    #if !defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
     typedef memory_pool<sizeof(node_cell)> node_allocator;
     static node_allocator & get_node_allocator() {
         LEAN_THREAD_PTR(node_allocator) g_allocator;
@@ -70,6 +76,7 @@ class rb_tree : public CMP {
             g_allocator.reset(new node_allocator());
         return *g_allocator;
     }
+    #endif
 
     int cmp(T const & v1, T const & v2) const {
         return CMP::operator()(v1, v2);
@@ -77,7 +84,11 @@ class rb_tree : public CMP {
 
     static node ensure_unshared(node && n) {
         if (n.is_shared()) {
+            #if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
+            return node(new node_cell(*n.m_ptr));
+            #else
             return node(new (get_node_allocator().allocate()) node_cell(*n.m_ptr));
+            #endif
         } else {
             return n;
         }
@@ -135,8 +146,13 @@ class rb_tree : public CMP {
     }
 
     node insert(node && n, T const & v) {
-        if (!n)
+        if (!n) {
+            #if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
+            return node(new node_cell(v));
+            #else
             return node(new (get_node_allocator().allocate()) node_cell(v));
+            #endif
+        }
         node h = ensure_unshared(n.steal());
 
         int c = cmp(v, h->m_value);
@@ -374,8 +390,12 @@ public:
 
 template<typename T, typename CMP>
 void rb_tree<T, CMP>::node_cell::dealloc() {
+    #if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
+    delete this;
+    #else
     this->~node_cell();
     get_node_allocator().recycle(this);
+    #endif
 }
 
 template<typename T, typename CMP>