diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean
index 14ca50d4dc..6705dd3561 100644
--- a/library/logic/classes/decidable.lean
+++ b/library/logic/classes/decidable.lean
@@ -99,7 +99,7 @@ end decidable
 inductive decidable_eq [class] (A : Type) : Type :=
 intro : (Π x y : A, decidable (x = y)) → decidable_eq A
 
-theorem decidable_eq_to_decidable [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) :=
+theorem of_decidable_eq [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) :=
 decidable_eq.rec (λ H, H) H x y
 
-coercion decidable_eq_to_decidable : decidable_eq
+coercion of_decidable_eq : decidable_eq