1 files changed, 4 insertions, 15 deletions
diff --git a/src/util/hash.h b/src/util/hash.h
index af468e25b..b04fb8bb5 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -20,13 +20,10 @@
 #ifndef __CVC4__HASH_H
 #define __CVC4__HASH_H
 
-// in case it's not been declared as a namespace yet
-namespace __gnu_cxx {}
+#include <functional>
+#include <string>
 
-#include <ext/hash_map>
-#include <ext/hash_set>
-
-namespace __gnu_cxx {
+namespace std {
 
 #ifdef CVC4_NEED_HASH_UINT64_T
 // on some versions and architectures of GNU C++, we need a
@@ -39,18 +36,10 @@ struct hash<uint64_t> {
 };/* struct hash<uint64_t> */
 #endif /* CVC4_NEED_HASH_UINT64_T */
 
-}/* __gnu_cxx namespace */
-
-// hackish: treat hash stuff as if it were in std namespace
-namespace std { using namespace __gnu_cxx; }
+}/* std namespace */
 
 namespace CVC4 {
 
-struct StringHashFunction {
-  size_t operator()(const std::string& str) const {
-    return __gnu_cxx::hash<const char*>()(str.c_str());
-  }
-};/* struct StringHashFunction */
 
 template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
 struct PairHashFunction {