From ad43d9177b7025b5f949a2a9e44b8604fe1deaf8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Apr 2014 11:09:13 -0700
Subject: [PATCH] refactor(util/name_set): implement name_sets using red black
 trees instead of hashtables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/name_set.cpp | 2 +-
 src/util/name_set.h   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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.