diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean
index 93b5958ae..8d50af170 100644
--- a/hott/algebra/category/functor/yoneda.hlean
+++ b/hott/algebra/category/functor/yoneda.hlean
@@ -17,7 +17,7 @@ namespace yoneda
     However, we don't want to have them globally, because that will unfold the composition g ∘ f
     in a Category to category.category.comp g f
   -/
-  local attribute Category.to.precategory category.to_precategory [constructor]
+  local attribute category.to_precategory [constructor]
 
   -- should this be defined as "yoneda_embedding Cᵒᵖ"?
   definition contravariant_yoneda_embedding [constructor] [reducible]
diff --git a/hott/algebra/category/limits/functor_preserve.hlean b/hott/algebra/category/limits/functor_preserve.hlean
index fd42ebc35..d29f6fb66 100644
--- a/hott/algebra/category/limits/functor_preserve.hlean
+++ b/hott/algebra/category/limits/functor_preserve.hlean
@@ -50,7 +50,7 @@ namespace category
 
   /- yoneda preserves existing limits -/
 
-  local attribute Category.to.precategory category.to_precategory [constructor]
+  local attribute category.to_precategory [constructor]
 
   definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (y : cone_obj F)
     [H : is_terminal y] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) :
diff --git a/hott/algebra/category/limits/set.hlean b/hott/algebra/category/limits/set.hlean
index ac65e8f52..3d2d2c2ea 100644
--- a/hott/algebra/category/limits/set.hlean
+++ b/hott/algebra/category/limits/set.hlean
@@ -11,7 +11,6 @@ import .colimits ..constructions.set hit.set_quotient
 open eq functor is_trunc sigma pi sigma.ops trunc set_quotient
 
 namespace category
-  local attribute Category.to.precategory [unfold 1]
   local attribute category.to_precategory [unfold 2]
 
   definition is_complete_set_cone.{u v w} [constructor]
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index b59b577e7..53bddbf99 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -27,7 +27,7 @@ namespace algebra
   -- coercions between them anymore.
   -- So, an application such as (@mul A G g h) in the following definition
   -- is type incorrect if the coercion is not added (explicitly or implicitly).
-  local attribute group.to.has_mul [coercion]
+  definition group.to_has_mul [coercion] {A : Type} (H : group A) : has_mul A := _
   local attribute group.to_has_inv [coercion]
 
   universe variable l
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index c004028b6..142f3f32d 100644
--- a/hott/types/int/basic.hlean
+++ b/hott/types/int/basic.hlean
@@ -380,7 +380,8 @@ calc
     ... = nat_abs a : abstr_repr
 
 theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
-show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add_comm ▸ rfl
+show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0,
+by rewrite [nat.add_comm (pr1 p)]
 
 theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
 calc      pr1 p + pr1 q + pr2 q + pr2 p
diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index 6b11d9627..167bdb609 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -71,7 +71,7 @@ theorem one_pow : ∀ n : ℕ, 1^n = (1:A)
 theorem pow_add (a : A) (m n : ℕ) : a^(m + n) = a^m * a^n :=
 begin
   induction n with n ih,
-    {rewrite [nat.add_zero, pow_zero, mul_one]},
+    {krewrite [nat.add_zero, pow_zero, mul_one]},
   rewrite [add_succ, *pow_succ', ih, mul.assoc]
 end
 
@@ -171,7 +171,7 @@ include s
 theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 :=
   begin
     induction n,
-    rewrite pow_zero,
+    krewrite pow_zero,
     apply zero_lt_one,
     rewrite pow_succ',
     apply mul_pos,
@@ -181,7 +181,7 @@ theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 :=
 theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : a ^ n ≥ 1 :=
   begin
     induction n,
-    rewrite pow_zero,
+    krewrite pow_zero,
     apply le.refl,
     rewrite [pow_succ', -mul_one 1],
     apply mul_le_mul v_0 H zero_le_one,
diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean
index bcde5a2ea..dbf2bf56e 100644
--- a/library/algebra/ring_power.lean
+++ b/library/algebra/ring_power.lean
@@ -21,7 +21,7 @@ theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) :=
 have h₁ : ∀ m : nat, (0 : A)^(succ m) = (0 : A),
   begin
     intro m, induction m,
-      rewrite pow_one,
+      krewrite pow_one,
       apply zero_mul
   end,
 obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos,
@@ -45,7 +45,7 @@ or.elim (eq_zero_or_pos m)
       begin
         intro m,
         induction m with m ih,
-          {rewrite pow_one; intros; assumption},
+          {krewrite pow_one; intros; assumption},
         rewrite pow_succ,
         intro H,
         cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄,
@@ -73,7 +73,7 @@ or.elim (eq_zero_or_pos m)
       begin
         intro m,
         induction m with m ih,
-          {rewrite pow_one; assumption},
+          { krewrite pow_one; assumption },
         rewrite pow_succ,
         apply division_ring.mul_ne_zero H ih
       end,
@@ -136,7 +136,7 @@ monoid_has_pow_nat
 theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n :=
 begin
   induction n with n ih,
-    rewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)],
+    krewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)],
   rewrite [*pow_succ, abs_mul, ih]
 end
 
@@ -149,7 +149,7 @@ include s
 theorem field.div_pow (a : A) {b : A} {n : ℕ} (bnz : b ≠ 0) : (a / b)^n = a^n / b^n :=
 begin
   induction n with n ih,
-    rewrite [*pow_zero, div_one],
+    krewrite [*pow_zero, div_one],
   have bnnz : b^n ≠ 0, from division_ring.pow_ne_zero_of_ne_zero bnz,
   rewrite [*pow_succ, ih, !field.div_mul_div bnz bnnz]
 end
@@ -163,7 +163,7 @@ include s
 theorem div_pow (a : A) {b : A} {n : ℕ} : (a / b)^n = a^n / b^n :=
 begin
   induction n with n ih,
-    rewrite [*pow_zero, div_one],
+    krewrite [*pow_zero, div_one],
   rewrite [*pow_succ, ih, div_mul_div]
 end
 
diff --git a/library/data/complex.lean b/library/data/complex.lean
index 491544041..1c4e9592f 100644
--- a/library/data/complex.lean
+++ b/library/data/complex.lean
@@ -30,10 +30,10 @@ protected proposition eta (z : ℂ) : complex.mk (complex.re z) (complex.im z) =
 by cases z; exact rfl
 
 definition of_real [coercion] (x : ℝ) : ℂ := complex.mk x 0
-definition of_rat [coercion] (q : ℚ) : ℂ := rat.to.complex q
-definition of_int [coercion] (i : ℤ) : ℂ := int.to.complex i
-definition of_nat [coercion] (n : ℕ) : ℂ := nat.to.complex n
-definition of_num [coercion] [reducible] (n : num) : ℂ := num.to.complex n
+definition of_rat [coercion] (q : ℚ) : ℂ := q
+definition of_int [coercion] (i : ℤ) : ℂ := i
+definition of_nat [coercion] (n : ℕ) : ℂ := n
+definition of_num [coercion] [reducible] (n : num) : ℂ := n
 
 protected definition prio : num := num.pred real.prio
 
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 9b21a8b40..8ea0bef1b 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -99,7 +99,7 @@ calc
       ... < 0                 : neg_neg_of_pos this
 
 protected theorem zero_div (b : ℤ) : 0 / b = 0 :=
-by rewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero]
+by krewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero]
 
 protected theorem div_zero (a : ℤ) : a / 0 = 0 :=
 by rewrite [div_def, sign_zero, zero_mul]
diff --git a/library/data/int/power.lean b/library/data/int/power.lean
index a97d65461..abec75efc 100644
--- a/library/data/int/power.lean
+++ b/library/data/int/power.lean
@@ -23,7 +23,7 @@ theorem of_nat_pow (a n : ℕ) : of_nat (a^n) = (of_nat a)^n :=
 begin
   induction n with n ih,
     apply eq.refl,
-  rewrite [pow_succ, pow_succ, of_nat_mul, ih]
+  krewrite [pow_succ, pow_succ, of_nat_mul, ih]
 end
 
 end int
diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean
index 6784624bf..4307166cf 100644
--- a/library/data/nat/bigops.lean
+++ b/library/data/nat/bigops.lean
@@ -35,7 +35,7 @@ proposition sum_range_def (m n : ℕ) (f : ℕ → A) :
 
 proposition sum_range_self (m : ℕ) (f : ℕ → A) :
             (∑ i = m...m, f i) = f m :=
-  by rewrite [↑sum_range, succ_sub !le.refl, nat.sub_self, sum_up_to_one, zero_add]
+  by krewrite [↑sum_range, succ_sub !le.refl, nat.sub_self, sum_up_to_one, zero_add]
 
 proposition sum_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) :
             (∑ i = m...succ n, f i) = (∑ i = m...n, f i) + f (succ n) :=
@@ -126,7 +126,7 @@ proposition prod_range_def (m n : ℕ) (f : ℕ → A) :
 
 proposition prod_range_self (m : ℕ) (f : ℕ → A) :
             (∏ i = m...m, f i) = f m :=
-by rewrite [↑prod_range, succ_sub !le.refl, nat.sub_self, prod_up_to_one, zero_add]
+by krewrite [↑prod_range, succ_sub !le.refl, nat.sub_self, prod_up_to_one, zero_add]
 
 proposition prod_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) :
             (∏ i = m...succ n, f i) = (∏ i = m...n, f i) * f (succ n) :=
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index 7b093734b..b97ad5c8f 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -24,7 +24,7 @@ or.elim (eq_zero_or_pos m)
       begin
         intro m,
         induction m with m ih,
-          {rewrite pow_one; intros; assumption},
+          {krewrite pow_one; intros; assumption},
         rewrite pow_succ,
         intro H,
         cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄,
@@ -53,7 +53,7 @@ theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
 
 theorem mul_self_eq_pow_2 (a : nat) : a * a = a ^ 2 :=
 show a * a = a ^ (succ (succ zero)), from
-by rewrite [*pow_succ, *pow_zero, mul_one]
+by krewrite [*pow_succ, *pow_zero, mul_one]
 
 theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a ^ b = a ^ c → b = c
 | a 0        0        h₁ h₂ := rfl
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 837ab5afe..4bf4b982e 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -353,8 +353,8 @@ namespace rat
 /- operations -/
 
 definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧
-definition of_nat [coercion] (n : ℕ) : ℚ := nat.to.rat n
-definition of_num [coercion] [reducible] (n : num) : ℚ := num.to.rat n
+definition of_nat [coercion] (n : ℕ) : ℚ := n
+definition of_num [coercion] [reducible] (n : num) : ℚ := n
 
 protected definition prio := num.pred int.prio
 
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 472a7c118..9e6ebbed8 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -1092,8 +1092,8 @@ has_sub.mk real.sub
 open rat -- no coercions before
 
 definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a)
-definition of_int [coercion] (i : ℤ) : ℝ := int.to.real i
-definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real n
+definition of_int [coercion] (i : ℤ) : ℝ := i
+definition of_nat [coercion] (n : ℕ) : ℝ := n
 definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n)
 
 definition real_has_zero [reducible] [instance] [priority real.prio] : has_zero real :=
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 9f7c9bf0c..45df21ba8 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -367,11 +367,11 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) :
       apply converges_to_seq_constant,
       rewrite -{0}zero_add,
       apply add_converges_to_seq,
-      rewrite -(mul_zero K),
+      krewrite -(mul_zero K),
       apply mul_left_converges_to_seq,
       apply abs_sub_converges_to_seq_of_converges_to_seq,
       exact HY,
-      rewrite -(mul_zero (abs y)),
+      krewrite -(mul_zero (abs y)),
       apply mul_left_converges_to_seq,
       apply abs_sub_converges_to_seq_of_converges_to_seq,
       exact HX
diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean
index 464de0efc..84eda84b2 100644
--- a/library/theories/combinatorics/choose.lean
+++ b/library/theories/combinatorics/choose.lean
@@ -58,7 +58,7 @@ begin
   induction n with [n, ih],
     {apply rfl},
   change choose (succ n) (succ 0) = succ n,
-  rewrite [choose_succ_succ, ih, choose_zero_right]
+  krewrite [choose_succ_succ, ih, choose_zero_right]
 end
 
 theorem choose_pos {n : ℕ} : ∀ {k : ℕ}, k ≤ n → choose n k > 0 :=
@@ -87,7 +87,7 @@ begin
          krewrite [one_mul, choose_zero_succ, choose_eq_zero_of_lt H, zero_mul]}},
   intro k,
   cases k with k',
-    {rewrite [choose_zero_right, choose_one_right]},
+    {krewrite [choose_zero_right, choose_one_right]},
   rewrite [choose_succ_succ (succ n), right_distrib, -ih (succ k')],
   rewrite [choose_succ_succ at {1}, left_distrib, *succ_mul (succ n), mul_succ, -ih k'],
   rewrite [*add.assoc, add.left_comm (choose n _)]
diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean
index 78625b908..a7a9a4106 100644
--- a/library/theories/number_theory/prime_factorization.lean
+++ b/library/theories/number_theory/prime_factorization.lean
@@ -246,7 +246,7 @@ theorem mult_pow_eq_zero_of_prime_of_ne {p q : ℕ} (primep : prime p) (primeq :
   (pneq : p ≠ q) (i : ℕ) : mult p (q^i) = 0 :=
 begin
   induction i with i ih,
-    {rewrite [pow_zero, mult_one_right]},
+    {krewrite [pow_zero, mult_one_right]},
   have qpos : q > 0, from pos_of_prime primeq,
   have qipos : q^i > 0, from !pow_pos_of_pos qpos,
   rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep
diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp
index 8b4986711..dec400055 100644
--- a/src/library/tc_multigraph.cpp
+++ b/src/library/tc_multigraph.cpp
@@ -59,30 +59,8 @@ struct add_edge_fn {
         m_graph.m_edges.insert(edge, src);
     }
 
-
-    static name compose_name_core(name const & src, name const & tgt) {
-        return src + name("to") + tgt;
-    }
-
-    static name compose_name(name const & p, name const & src, name const & tgt) {
-        if (is_prefix_of(p, tgt))
-            return compose_name_core(src, tgt.replace_prefix(p, name()));
-        else if (p.is_atomic())
-            return compose_name_core(src, tgt);
-        else
-            return compose_name(p.get_prefix(), src, tgt);
-    }
-
-    static name compose_name(name const & src, name const & tgt) {
-        if (src.is_atomic())
-            return compose_name_core(src, tgt);
-        else
-            return compose_name(src.get_prefix(), src, tgt);
-    }
-
-    name compose(name const & src, name const & e1, name const & e2, name const & tgt) {
-        name n = compose_name(src, tgt);
-        pair<environment, name> env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional<name>(n));
+    name compose(name const & base_name, name const & e1, name const & e2) {
+        pair<environment, name> env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional<name>(base_name));
         m_env = env_e.first;
         return env_e.second;
     }
@@ -90,6 +68,7 @@ struct add_edge_fn {
     pair<environment, list<tc_edge>> operator()(name const & src, name const & edge, name const & tgt) {
         buffer<tc_edge> new_edges;
         if (auto preds = m_graph.m_predecessors.find(src)) {
+            name base_name = edge.append_before("_trans_to_");
             for (name const & pred : *preds) {
                 if (pred == tgt)
                     continue; // avoid loops
@@ -97,7 +76,7 @@ struct add_edge_fn {
                     for (pair<name, name> const & p : *pred_succ) {
                         if (p.second != src)
                             continue;
-                        name new_e = compose(pred, p.first, edge, tgt);
+                        name new_e = compose(base_name, p.first, edge);
                         new_edges.emplace_back(pred, new_e, tgt);
                     }
                 }
@@ -107,15 +86,16 @@ struct add_edge_fn {
         buffer<tc_edge> new_back_edges;
         new_back_edges.append(new_edges);
         if (auto succs = m_graph.m_successors.find(tgt)) {
+            name base_name = edge.append_before("_trans_of_");
             for (pair<name, name> const & p : *succs) {
                 if (src == p.second)
                     continue; // avoid loops
-                name new_e = compose(src, edge, p.first, p.second);
+                name new_e = compose(base_name, edge, p.first);
                 new_edges.emplace_back(src, new_e, p.second);
                 for (auto const & back_edge : new_back_edges) {
                     if (back_edge.m_from != p.second)
                         continue;
-                    name new_e = compose(back_edge.m_from, back_edge.m_cnst, p.first, p.second);
+                    name new_e = compose(base_name, back_edge.m_cnst, p.first);
                     new_edges.emplace_back(back_edge.m_from, new_e, p.second);
                 }
             }
diff --git a/tests/lean/852.hlean b/tests/lean/852.hlean
index d6954c0b4..7fc17ae67 100644
--- a/tests/lean/852.hlean
+++ b/tests/lean/852.hlean
@@ -2,4 +2,4 @@ import algebra.category.functor.equivalence
 
 -- print prefix category.equivalence
 
-check @category.equivalence.to._Fun
+-- check @category.equivalence.to._Fun
diff --git a/tests/lean/852.hlean.expected.out b/tests/lean/852.hlean.expected.out
index ce53e0e8b..e69de29bb 100644
--- a/tests/lean/852.hlean.expected.out
+++ b/tests/lean/852.hlean.expected.out
@@ -1,6 +0,0 @@
-category.equivalence.to._Fun :
-  Π {C : category.Precategory} {D : category.Precategory} (c : category.equivalence C D)
-  {a b : category.Precategory.carrier C},
-    category.hom a b →
-    category.hom (functor.to_fun_ob (category.equivalence.to_functor c) a)
-      (functor.to_fun_ob (category.equivalence.to_functor c) b)
diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out
index 71813e21b..6adfc8960 100644
--- a/tests/lean/binder_overload.lean.expected.out
+++ b/tests/lean/binder_overload.lean.expected.out
@@ -1,8 +1,15 @@
 {x : ℕ ∈ S | x > 0} : set ℕ
 {x : ℕ ∈ s | x > 0} : finset ℕ
-@set.sep.{1} nat (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero)) S : set.{1} nat
+@set.sep.{1} nat
+  (λ (x : nat),
+     @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
+       (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
+  S :
+  set.{1} nat
 @finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b)
-  (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero))
-  (λ (a : nat), nat.decidable_lt (@zero.{1} nat _source.to.has_zero) a)
+  (λ (x : nat),
+     @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
+       (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
+  (λ (a : nat), nat.decidable_lt (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6) a)
   s :
   finset.{1} nat
diff --git a/tests/lean/extra/show_goal.lean b/tests/lean/extra/show_goal.lean
index 5dba4c039..a5489e1a3 100644
--- a/tests/lean/extra/show_goal.lean
+++ b/tests/lean/extra/show_goal.lean
@@ -13,7 +13,7 @@ begin
     have ceq : c = 0, begin
       rewrite aeq0 at h₃,
       rewrite add_zero at h₃,
-      rewrite add_succ at h₃,
+      krewrite add_succ at h₃,
       krewrite add_zero at h₃,
       injection h₃, exact a_1
     end,
diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean/notation_priority.lean.expected.out
index af4e2ac54..9db0fe887 100644
--- a/tests/lean/notation_priority.lean.expected.out
+++ b/tests/lean/notation_priority.lean.expected.out
@@ -1,4 +1,4 @@
-@add.{1} nat _source.to.has_add a b : nat
-@add.{1} int _source.to.has_add_1 i j : int
-@add.{1} nat _source.to.has_add a b : nat
-@add.{1} int _source.to.has_add_1 i j : int
+@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 a b : nat
+@add.{1} int int._trans_of_linear_ordered_comm_ring_16 i j : int
+@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 a b : nat
+@add.{1} int int._trans_of_linear_ordered_comm_ring_16 i j : int
diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out
index 205e9cc63..d40a12b76 100644
--- a/tests/lean/pp_all.lean.expected.out
+++ b/tests/lean/pp_all.lean.expected.out
@@ -1,8 +1,9 @@
 a + of_num b = 10 : Prop
 @eq.{1} nat
-  (@add.{1} nat _source.to.has_add ((λ (x : nat), x) a)
+  (@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 _source.to.has_add
-     (@bit1.{1} nat _source.to.has_one _source.to.has_add
-        (@bit0.{1} nat _source.to.has_add (@one.{1} nat _source.to.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)))) :
   Prop
diff --git a/tests/lean/run/collision_bug.lean b/tests/lean/run/collision_bug.lean
new file mode 100644
index 000000000..14c62b62e
--- /dev/null
+++ b/tests/lean/run/collision_bug.lean
@@ -0,0 +1,2 @@
+import theories.measure_theory.sigma_algebra
+import data.int.order
diff --git a/tests/lean/run/inj_tac.lean b/tests/lean/run/inj_tac.lean
index 6d6bdb19e..ac8b1625c 100644
--- a/tests/lean/run/inj_tac.lean
+++ b/tests/lean/run/inj_tac.lean
@@ -38,6 +38,6 @@ example (a₁ a₂ a₃ b₁ b₂ b₃ : nat) : (a₁+2, a₂+3, a₃+1) = (b₁
 begin
   intro H, injection H with a₁b₁ sa₂b₂ a₃sb₃,
   esimp at *,
-  rewrite [a₁b₁, a₃sb₃, sa₂b₂],
+  krewrite [a₁b₁, a₃sb₃, -sa₂b₂],
   repeat (split | esimp)
 end