diff --git a/library/init/ordered_group.lean b/library/init/ordered_group.lean
index 2d4e0dc5c3..47ed260f5f 100644
--- a/library/init/ordered_group.lean
+++ b/library/init/ordered_group.lean
@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import init.group
 
+/- Make sure instances defined in this file have lower priority than the ones
+   defined for concrete structures -/
+set_option default_priority 100
+
 universe variable u
 
 class ordered_mul_cancel_comm_monoid (α : Type u)
diff --git a/library/init/ordered_ring.lean b/library/init/ordered_ring.lean
index 6b53c5d348..6afbbfd7ba 100644
--- a/library/init/ordered_ring.lean
+++ b/library/init/ordered_ring.lean
@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import init.ordered_group init.ring
 
+/- Make sure instances defined in this file have lower priority than the ones
+   defined for concrete structures -/
+set_option default_priority 100
+
 universe variable u
 
 structure ordered_semiring (α : Type u)
diff --git a/library/init/ring.lean b/library/init/ring.lean
index 12aee72050..03ddbe3ccf 100644
--- a/library/init/ring.lean
+++ b/library/init/ring.lean
@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import init.group
 
+/- Make sure instances defined in this file have lower priority than the ones
+   defined for concrete structures -/
+set_option default_priority 100
+
 universe variable u
 
 class distrib (α : Type u) extends has_mul α, has_add α :=