diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index aa6bc351f..8cbbd2aa8 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -7,7 +7,7 @@ endif()
 add_library(util trace.cpp debug.cpp name.cpp name_set.cpp name_generator.cpp
   exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
   safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
-  script_state.cpp script_exception.cpp splay_map.cpp rb_map.cpp lua.cpp
+  script_state.cpp script_exception.cpp rb_map.cpp lua.cpp
   luaref.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp ${THREAD_CPP})
 
 target_link_libraries(util ${LEAN_LIBS})
diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 211c9ed63..c9912500e 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "util/script_state.h"
 #include "util/script_exception.h"
 #include "util/name.h"
-#include "util/splay_map.h"
+#include "util/rb_map.h"
 #include "util/lean_path.h"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
@@ -84,7 +84,7 @@ struct script_state::imp {
         luaL_openlibs(m_state);
         open_exception(m_state);
         open_name(m_state);
-        open_splay_map(m_state);
+        open_rb_map(m_state);
         open_extra(m_state);
 
         for (auto f : g_modules) {
diff --git a/src/util/splay_map.cpp b/src/util/splay_map.cpp
deleted file mode 100644
index 69a4bec1b..000000000
--- a/src/util/splay_map.cpp
+++ /dev/null
@@ -1,100 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/lua.h"
-#include "util/luaref.h"
-#include "util/splay_map.h"
-
-namespace lean {
-typedef splay_map<luaref, luaref, luaref_lt_proc> lua_splay_map;
-DECL_UDATA(lua_splay_map)
-
-static int mk_lua_splay_map(lua_State * L) {
-    lua_splay_map r;
-    return push_lua_splay_map(L, r);
-}
-
-static int lua_splay_map_size(lua_State * L) {
-    lua_pushinteger(L, to_lua_splay_map(L, 1).size());
-    return 1;
-}
-
-static int lua_splay_map_contains(lua_State * L) {
-    lua_pushboolean(L, to_lua_splay_map(L, 1).contains(luaref(L, 2)));
-    return 1;
-}
-
-static int lua_splay_map_empty(lua_State * L) {
-    lua_pushboolean(L, to_lua_splay_map(L, 1).empty());
-    return 1;
-}
-
-static int lua_splay_map_insert(lua_State * L) {
-    to_lua_splay_map(L, 1).insert(luaref(L, 2), luaref(L, 3));
-    return 0;
-}
-
-static int lua_splay_map_erase(lua_State * L) {
-    to_lua_splay_map(L, 1).erase(luaref(L, 2));
-    return 0;
-}
-
-static int lua_splay_map_find(lua_State * L) {
-    lua_splay_map & m = to_lua_splay_map(L, 1);
-    luaref const * val = m.find(luaref(L, 2));
-    if (val) {
-        lean_assert(val->get_state() == L);
-        val->push();
-    } else {
-        lua_pushnil(L);
-    }
-    return 1;
-}
-
-static int lua_splay_map_copy(lua_State * L) {
-    return push_lua_splay_map(L, to_lua_splay_map(L, 1));
-}
-
-static int lua_splay_map_for_each(lua_State * L) {
-    // Remark: we take a copy of the map to make sure
-    // for_each will not crash if the map is updated while being
-    // traversed.
-    // The copy operation is very cheap O(1).
-    lua_splay_map m(to_lua_splay_map(L, 1)); // map
-    luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
-    m.for_each([&](luaref const & k, luaref const & v) {
-        lua_pushvalue(L, 2); // push user-fun
-        k.push();
-        v.push();
-        pcall(L, 2, 0, 0);
-        });
-    return 0;
-}
-
-static const struct luaL_Reg lua_splay_map_m[] = {
-    {"__gc",            lua_splay_map_gc}, // never throws
-    {"__len",           safe_function<lua_splay_map_size> },
-    {"contains",        safe_function<lua_splay_map_contains>},
-    {"size",            safe_function<lua_splay_map_size>},
-    {"empty",           safe_function<lua_splay_map_empty>},
-    {"insert",          safe_function<lua_splay_map_insert>},
-    {"erase",           safe_function<lua_splay_map_erase>},
-    {"find",            safe_function<lua_splay_map_find>},
-    {"copy",            safe_function<lua_splay_map_copy>},
-    {"for_each",        safe_function<lua_splay_map_for_each>},
-    {0, 0}
-};
-
-void open_splay_map(lua_State * L) {
-    luaL_newmetatable(L, lua_splay_map_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, lua_splay_map_m, 0);
-
-    SET_GLOBAL_FUN(mk_lua_splay_map,          "splay_map");
-    SET_GLOBAL_FUN(lua_splay_map_pred,        "is_splay_map");
-}
-}