diff --git a/library/init/data/rbmap/default.lean b/library/init/data/rbmap/default.lean
new file mode 100644
index 0000000000..4d5a38b69a
--- /dev/null
+++ b/library/init/data/rbmap/default.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.data.rbtree init.data.rbmap.basic