diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index b8e0bc5432..e33f2e1909 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -431,8 +431,8 @@ variable {p q : Prop}
   else
     isFalse fun hq => absurd (Iff.mpr h hq) hp
 
-@[inline] def  decidable_of_decidable_of_eq [hp : Decidable p] (h : p = q) : Decidable q :=
-  h ▸ hp
+@[inline] def  decidable_of_decidable_of_eq [Decidable p] (h : p = q) : Decidable q :=
+  decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)
 end
 
 @[macroInline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) :=