diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 9e6ebbed8..9210d1464 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -1096,11 +1096,11 @@ 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 :=
-has_zero.mk (of_rat 0)
+definition real_has_zero [reducible] : has_zero real := has_zero.mk (of_rat 0)
+local attribute real_has_zero [instance] [priority real.prio]
 
-definition real_has_one [reducible] [instance] [priority real.prio] : has_one real :=
-has_one.mk (of_rat 1)
+definition real_has_one [reducible] : has_one real := has_one.mk (of_rat 1)
+local attribute real_has_one [instance] [priority real.prio]
 
 theorem real_zero_eq_rat_zero : (0:real) = of_rat (0:rat) :=
 rfl
@@ -1150,7 +1150,7 @@ protected definition comm_ring [reducible] : comm_ring ℝ :=
     fapply comm_ring.mk,
     exact real.add,
     exact real.add_assoc,
-    exact of_num 0,
+    exact 0,
     exact real.zero_add,
     exact real.add_zero,
     exact real.neg,
@@ -1158,7 +1158,7 @@ protected definition comm_ring [reducible] : comm_ring ℝ :=
     exact real.add_comm,
     exact real.mul,
     exact real.mul_assoc,
-    apply of_num 1,
+    apply 1,
     apply real.one_mul,
     apply real.mul_one,
     apply real.left_distrib,
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 837f0ff6b..1a8fb6ee2 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -13,6 +13,9 @@ open rat nat eq pnat
 
 local postfix `⁻¹` := pnat.inv
 
+local attribute real.real_has_zero [instance] [priority real.prio]
+local attribute real.real_has_one [instance] [priority real.prio]
+
 namespace rat_seq
 definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
 
@@ -1089,7 +1092,7 @@ protected theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
         apply (or.inr (quot.exact H'))
       end)))
 
-definition ordered_ring [reducible] [instance] : ordered_ring ℝ :=
+definition ordered_ring [reducible] [trans_instance] : ordered_ring ℝ :=
 ⦃ ordered_ring, real.comm_ring,
   le_refl := real.le_refl,
   le_trans := @real.le_trans,
diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean
index 386c1ec80..b3f0372fa 100644
--- a/library/theories/analysis/metric_space.lean
+++ b/library/theories/analysis/metric_space.lean
@@ -204,6 +204,7 @@ proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ
       note Hallm' := of_mem_of_all Hmem Hall,
       apply le_neg_of_le_neg,
       esimp, esimp at Hallm',
+/-
       have Heqs : (λ (a b : real), classical.prop_decidable (@le.{1} real real.real_has_le a b))
                    =
                    (@decidable_le.{1} real
@@ -216,6 +217,7 @@ proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ
         apply dec_prf_eq
       end,
       rewrite -Heqs,
+-/
       exact Hallm'
     end,
     cases em (n < N) with Elt Ege,