diff --git a/src/util/name_set.cpp b/src/util/name_set.cpp
index 03d3df124..15e270925 100644
--- a/src/util/name_set.cpp
+++ b/src/util/name_set.cpp
@@ -11,7 +11,7 @@ name mk_unique(name_set const & s, name const & suggestion) {
     name n = suggestion;
     int i  = 1;
     while (true) {
-        if (s.find(n) == s.end())
+        if (!s.contains(n))
             return n;
         n = name(suggestion, i);
         i++;
diff --git a/src/util/name_set.h b/src/util/name_set.h
index e28a05a44..04b89eccd 100644
--- a/src/util/name_set.h
+++ b/src/util/name_set.h
@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <unordered_set>
+#include "util/rb_tree.h"
 #include "util/name.h"
 namespace lean {
-typedef std::unordered_set<name, name_hash, name_eq> name_set;
+typedef rb_tree<name, name_quick_cmp> name_set;
 /**
    \brief Make a name that does not occur in \c s, based on
    the given suggestion.