From 650a08945cfa1ca5f76bfd6e0385e9bb0cceac28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Jun 2016 16:11:55 -0700
Subject: [PATCH] perf(library/meta/rb_map): mark rb_map.mk as inline

---
 library/meta/rb_map.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/meta/rb_map.lean b/library/meta/rb_map.lean
index d2399a6fc8..bbb8966ecf 100644
--- a/library/meta/rb_map.lean
+++ b/library/meta/rb_map.lean
@@ -18,7 +18,7 @@ meta_constant min {key : Type} {data : Type}            : rb_map key data → op
 meta_constant max {key : Type} {data : Type}            : rb_map key data → option data
 meta_constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
 
-meta_definition mk (key : Type) [has_cmp key] (data : Type) : rb_map key data :=
+inline meta_definition mk (key : Type) [has_cmp key] (data : Type) : rb_map key data :=
 mk_core data has_cmp.cmp
 
 open list
@@ -32,7 +32,7 @@ meta_definition nat_map (data : Type) := rb_map nat data
 namespace nat_map
   export rb_map (hiding mk)
 
-  meta_definition mk (data : Type) : nat_map data :=
+  inline meta_definition mk (data : Type) : nat_map data :=
   rb_map.mk nat data
 end nat_map
 
@@ -40,6 +40,6 @@ meta_definition name_map (data : Type) := rb_map name data
 namespace name_map
   export rb_map (hiding mk)
 
-  meta_definition mk (data : Type) : name_map data :=
+  inline meta_definition mk (data : Type) : name_map data :=
   rb_map.mk name data
 end name_map