diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 8b2d806543..cd2bdec726 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -366,7 +366,7 @@ section discrete_field
       or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
   -/
 
-  definition discrete_field.to_integral_domain [trans_instance] :
+  definition discrete_field.to_integral_domain [instance] :
     integral_domain A :=
   ⦃ integral_domain, s,
     eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 50564ac0f5..614105c569 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -324,12 +324,12 @@ section group
 
 end group
 
-definition group.to_left_cancel_semigroup [trans_instance] [s : group A] :
+definition group.to_left_cancel_semigroup [instance] [s : group A] :
     left_cancel_semigroup A :=
 ⦃ left_cancel_semigroup, s,
   mul_left_cancel := @mul_left_cancel A s ⦄
 
-definition group.to_right_cancel_semigroup [trans_instance] [s : group A] :
+definition group.to_right_cancel_semigroup [instance] [s : group A] :
     right_cancel_semigroup A :=
 ⦃ right_cancel_semigroup, s,
   mul_right_cancel := @mul_right_cancel A s ⦄
@@ -466,11 +466,11 @@ section add_group
   by inst_simp
   -/
 
-  definition add_group.to_left_cancel_semigroup [trans_instance] : add_left_cancel_semigroup A :=
+  definition add_group.to_left_cancel_semigroup [instance] : add_left_cancel_semigroup A :=
   ⦃ add_left_cancel_semigroup, s,
     add_left_cancel := @add_left_cancel A s ⦄
 
-  definition add_group.to_add_right_cancel_semigroup [trans_instance] :
+  definition add_group.to_add_right_cancel_semigroup [instance] :
     add_right_cancel_semigroup A :=
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 784ad92393..804b802b80 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -114,7 +114,7 @@ section
   private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
     lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
 
-  definition order_pair.to_strict_order [trans_instance] : strict_order A :=
+  definition order_pair.to_strict_order [instance] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
   theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
@@ -188,7 +188,7 @@ section strong_order_pair
   show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
 end strong_order_pair
 
-definition strong_order_pair.to_order_pair [trans_instance]
+definition strong_order_pair.to_order_pair [instance]
     [s : strong_order_pair A] : order_pair A :=
 ⦃ order_pair, s,
   lt_irrefl := lt_irrefl',
@@ -203,7 +203,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak
 structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
     linear_weak_order A
 
-definition linear_strong_order_pair.to_linear_order_pair [trans_instance]
+definition linear_strong_order_pair.to_linear_order_pair [instance]
     [s : linear_strong_order_pair A] : linear_order_pair A :=
 ⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄
 
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index e845b8a4fe..575d4a8a38 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -469,7 +469,7 @@ section discrete_linear_ordered_field
       (assume H' : ¬ y < x,
         decidable.tt (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
 
-  definition discrete_linear_ordered_field.to_discrete_field [trans_instance] :  discrete_field A :=
+  definition discrete_linear_ordered_field.to_discrete_field [instance] :  discrete_field A :=
      ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄
 
     theorem pos_of_one_div_pos (H : 0 < 1 / a) : 0 < a :=
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 0e80e1d556..be073f6055 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -276,7 +276,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [ordered_comm_group A] {a b c :
 have H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
 sorry -- by rewrite *neg_add_cancel_left at H'; exact H'
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ⦃ ordered_cancel_comm_monoid, s,
   add_left_cancel       := @add.left_cancel A _,
   add_right_cancel      := @add.right_cancel A _,
@@ -781,7 +781,7 @@ structure decidable_linear_ordered_comm_group [class] (A : Type)
     (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
 
 definition decidable_linear_ordered_comm_group.to_ordered_comm_group
-      [trans_instance]
+      [instance]
    (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
 ⦃ ordered_comm_group, s,
   le_of_lt := @le_of_lt A _,
@@ -789,7 +789,7 @@ definition decidable_linear_ordered_comm_group.to_ordered_comm_group
   lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄
 
 definition decidable_linear_ordered_comm_group.to_decidable_linear_ordered_cancel_comm_monoid
-    [trans_instance] (A : Type) [s : decidable_linear_ordered_comm_group A] :
+    [instance] (A : Type) [s : decidable_linear_ordered_comm_group A] :
   decidable_linear_ordered_cancel_comm_monoid A :=
 ⦃ decidable_linear_ordered_cancel_comm_monoid, s,
     @ordered_comm_group.to_ordered_cancel_comm_monoid A _ ⦄
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 739ebaca73..186183e9e2 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -271,7 +271,7 @@ begin
 end
 -/
 
-definition ordered_ring.to_ordered_semiring [trans_instance]
+definition ordered_ring.to_ordered_semiring [instance]
     [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
@@ -371,7 +371,7 @@ structure linear_ordered_ring [class] (A : Type)
     extends ordered_ring A, linear_strong_order_pair A :=
   (zero_lt_one : lt zero one)
 
-definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance]
+definition linear_ordered_ring.to_linear_ordered_semiring [instance]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=
 ⦃ linear_ordered_semiring, s,
@@ -428,7 +428,7 @@ lt.by_cases
 -/
 
 -- Linearity implies no zero divisors. Doesn't need commutativity.
-definition linear_ordered_comm_ring.to_integral_domain [trans_instance]
+definition linear_ordered_comm_ring.to_integral_domain [instance]
     [s: linear_ordered_comm_ring A] : integral_domain A :=
 ⦃ integral_domain, s,
   eq_zero_or_eq_zero_of_mul_eq_zero :=
@@ -535,7 +535,7 @@ structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_o
     decidable_linear_ordered_comm_group A
 
 definition decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring
-    [trans_instance] [s : decidable_linear_ordered_comm_ring A] :
+    [instance] [s : decidable_linear_ordered_comm_ring A] :
   decidable_linear_ordered_semiring A :=
 ⦃decidable_linear_ordered_semiring, s, @linear_ordered_ring.to_linear_ordered_semiring A _⦄
 
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index acf3139a2b..c9845fc005 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -196,7 +196,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc
 show 0 * a = 0, from  (add.left_cancel this)⁻¹
 -/
 
-definition ring.to_semiring [trans_instance] [s : ring A] : semiring A :=
+definition ring.to_semiring [instance] [s : ring A] : semiring A :=
 ⦃ semiring, s,
   mul_zero := ring.mul_zero,
   zero_mul := ring.zero_mul ⦄
@@ -289,7 +289,7 @@ end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-definition comm_ring.to_comm_semiring [trans_instance] [s : comm_ring A] : comm_semiring A :=
+definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
 ⦃ comm_semiring, s,
   mul_zero := mul_zero,
   zero_mul := zero_mul ⦄
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index d934c346ed..fe878b9bee 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -252,7 +252,7 @@ nat.cases_on n (by simp)
           !succ_ne_zero))
 -/
 
-protected definition comm_semiring [trans_instance] : comm_semiring nat :=
+protected definition comm_semiring [instance] : comm_semiring nat :=
 ⦃comm_semiring,
  add            := nat.add,
  add_assoc      := nat.add_assoc,
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index d7160c4741..8c68781d2e 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -93,7 +93,7 @@ mul.comm k m ▸ mul.comm k n ▸ nat.mul_lt_mul_of_pos_left H Hk
 
 /- nat is an instance of a linearly ordered semiring and a lattice -/
 
-protected definition decidable_linear_ordered_semiring [trans_instance] :
+protected definition decidable_linear_ordered_semiring [instance] :
 decidable_linear_ordered_semiring nat :=
 ⦃ decidable_linear_ordered_semiring, nat.comm_semiring,
   add_left_cancel            := @nat.add_left_cancel,
diff --git a/src/library/class.cpp b/src/library/class.cpp
index e69c7d90b8..3db852692f 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -429,10 +429,6 @@ void initialize_class() {
     register_attribute(prio_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
           return add_instance(env, d, prio, persistent);
         }));
-
-    register_attribute(prio_attribute("trans_instance", "transitive type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
-          return add_trans_instance(env, d, prio, persistent);
-        }));
 }
 
 void finalize_class() {
diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out
index d40a12b76f..0ca48d7bbc 100644
--- a/tests/lean/pp_all.lean.expected.out
+++ b/tests/lean/pp_all.lean.expected.out
@@ -1,9 +1,6 @@
 a + of_num b = 10 : Prop
 @eq.{1} nat
-  (@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 ((λ (x : nat), x) a)
-     (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
-  (@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2
-     (@bit1.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22 nat._trans_of_decidable_linear_ordered_semiring_2
-        (@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2
-           (@one.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22)))) :
+  (@add.{1} nat nat_has_add ((λ (x : nat), x) a) (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one))))
+  (@bit0.{1} nat nat_has_add
+     (@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))) :
   Prop