diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3d1f9bda33..c2d345489d 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -315,7 +315,8 @@ theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
 
 theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
    (h₁ : Exists (fun x => p x)) (h₂ : ∀ (a : α), p a → b) : b :=
-  h₂ h₁.1 h₁.2
+  match h₁ with
+  | intro a h => h₂ a h
 
 /- Decidable -/