From 89bd5d6da2ee2e77cda83eedc97ed4f6df0753d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Aug 2020 14:49:20 -0700
Subject: [PATCH] fix: bug introduced today

---
 src/Lean/Elab/Binders.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 3c2b7df841..012ac01a42 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -465,7 +465,8 @@ else if letDecl.getKind == `Lean.Parser.Term.letPatDecl then do
   let stxNew  := if useLetExpr then stxNew else stxNew.updateKind `Lean.Parser.Term.«let!»;
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
 else if letDecl.getKind == `Lean.Parser.Term.letEqnsDecl then do
-  declNew ← liftMacroM $ expandLetEqnsDecl letDecl;
+  letDeclIdNew ← liftMacroM $ expandLetEqnsDecl letDecl;
+  let declNew := (stx.getArg 1).setArg 0 letDeclIdNew;
   let stxNew  := stx.setArg 1 declNew;
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
 else