diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean
index 426c9b3177..f8a8debf70 100644
--- a/library/init/data/rbmap/basic.lean
+++ b/library/init/data/rbmap/basic.lean
@@ -11,12 +11,10 @@ universes u v w
 def rbmap_lt {α : Type u} {β : Type v} (lt : α → α → Prop) (a b : α × β) : Prop :=
 lt a.1 b.1
 
-set_option auto_param.check_exists false
-
-def rbmap (α : Type u) (β : Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
+def rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) :=
 rbtree (α × β) (rbmap_lt lt)
 
-def mk_rbmap (α : Type u) (β : Type v) (lt : α → α → Prop . rbtree.default_lt) : rbmap α β lt :=
+def mk_rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : rbmap α β lt :=
 mk_rbtree (α × β) (rbmap_lt lt)
 
 namespace rbmap
@@ -85,10 +83,10 @@ to_value (m.find_entry k)
 def contains (m : rbmap α β lt) (k : α) : bool :=
 (find_entry m k).is_some
 
-def from_list (l : list (α × β)) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : rbmap α β lt :=
+def from_list (l : list (α × β)) (lt : α → α → Prop) [decidable_rel lt] : rbmap α β lt :=
 l.foldl (λ m p, insert m p.1 p.2)  (mk_rbmap α β lt)
 
 end rbmap
 
-def rbmap_of {α : Type u} {β : Type v} (l : list (α × β)) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : rbmap α β lt :=
+def rbmap_of {α : Type u} {β : Type v} (l : list (α × β)) (lt : α → α → Prop) [decidable_rel lt] : rbmap α β lt :=
 rbmap.from_list l lt
diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean
index e570bc7d75..c10c178154 100644
--- a/library/init/data/rbtree/basic.lean
+++ b/library/init/data/rbtree/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering
+import init.data.ordering.basic init.coe init.data.option.basic
 
 universes u v
 
@@ -162,12 +162,10 @@ end rbnode
 
 open rbnode
 
-set_option auto_param.check_exists false
-
-def rbtree (α : Type u) (lt : α → α → Prop . rbtree.default_lt) : Type u :=
+def rbtree (α : Type u) (lt : α → α → Prop) : Type u :=
 {t : rbnode α // t.well_formed lt }
 
-def mk_rbtree (α : Type u) (lt : α → α → Prop . rbtree.default_lt) : rbtree α lt :=
+def mk_rbtree (α : Type u) (lt : α → α → Prop) : rbtree α lt :=
 ⟨leaf, well_formed.leaf_wff lt⟩
 
 namespace rbtree
@@ -218,7 +216,7 @@ def find : rbtree α lt → α → option α
 def contains (t : rbtree α lt) (a : α) : bool :=
 (t.find a).is_some
 
-def from_list (l : list α) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : rbtree α lt :=
+def from_list (l : list α) (lt : α → α → Prop) [decidable_rel lt] : rbtree α lt :=
 l.foldl insert (mk_rbtree α lt)
 
 def all : rbtree α lt → (α → bool) → bool
@@ -235,5 +233,5 @@ subset t₁ t₂ && subset t₂ t₁
 
 end rbtree
 
-def rbtree_of {α : Type u} (l : list α) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : rbtree α lt :=
+def rbtree_of {α : Type u} (l : list α) (lt : α → α → Prop) [decidable_rel lt] : rbtree α lt :=
 rbtree.from_list l lt
diff --git a/library/init/data/rbtree/default.lean b/library/init/data/rbtree/default.lean
index 28812c78c3..3c9fd609c1 100644
--- a/library/init/data/rbtree/default.lean
+++ b/library/init/data/rbtree/default.lean
@@ -5,6 +5,3 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.rbtree.basic
-
-meta def rbtree.default_lt : tactic unit :=
-`[apply has_lt.lt]
diff --git a/library/init/lean/parser/macro.lean b/library/init/lean/parser/macro.lean
index de8050b6ac..3313a79314 100644
--- a/library/init/lean/parser/macro.lean
+++ b/library/init/lean/parser/macro.lean
@@ -43,14 +43,14 @@ structure resolved :=
 meta instance resolved.has_to_format : has_to_format resolved := ⟨λ r, to_fmt (r.decl, r.prefix)⟩
 
 structure resolve_cfg :=
-(global_scope : rbmap name syntax)
+(global_scope : rbmap name syntax (<))
 
-@[reducible] def resolve_map := rbmap syntax_id resolved
+@[reducible] def resolve_map := rbmap syntax_id resolved (<)
 
 structure resolve_state :=
 (resolve_map : resolve_map)
 
-def scope := rbmap (name × option macro_scope_id) syntax_id
+def scope := rbmap (name × option macro_scope_id) syntax_id (<)
 
 @[reducible] def resolve_m := parse_m resolve_cfg resolve_state
 
@@ -65,7 +65,7 @@ structure macro :=
 -- (elaborate : list syntax → expr → tactic expr)
 
 structure parse_state :=
-(macros : rbmap name macro)
+(macros : rbmap name macro (<))
 (resolve_cfg : resolve_cfg)
 
 -- identifiers in macro expansions are annotated with incremental tags