From 5af763f2433111a41fbcfbd98ab76e837febee9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Aug 2020 13:44:25 -0700
Subject: [PATCH] feat: use `checkNotAlreadyDeclared`

---
 src/Lean/Elab/LetRec.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 537c9a3dc2..6801550dc7 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Attributes
 import Lean.Elab.Binders
+import Lean.Elab.DeclModifiers
 
 namespace Lean
 namespace Elab
@@ -83,6 +84,9 @@ view.decls.mapIdxM fun i d => do
   headerLocalDecl ← getLocalDecl header.fnFVarId;
   forallBoundedTelescope headerLocalDecl.type header.numBinders fun xs type =>
      withDeclNameSuffix view.id do
+       currDeclName? ← getDeclName?;
+       let currDeclName := currDeclName?.get!;
+       checkNotAlreadyDeclared currDeclName;
        value ← elabTermEnsuringType view.value type;
        mkLambdaFVars xs value