diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean
index 3830ab5515..47a19b576e 100644
--- a/src/Init/Lean/Elab/TermBinders.lean
+++ b/src/Init/Lean/Elab/TermBinders.lean
@@ -305,7 +305,7 @@ let type     := expandOptType ref (decl.getArg 2);
 let val      := decl.getArg 4;
 elabLetDeclAux ref n binders type val body expectedType?
 
-@[builtinTermElab letDecl] def elabLetDecl : TermElab :=
+@[builtinTermElab «let»] def elabLetDecl : TermElab :=
 fun stx expectedType? => match_syntax stx with
 | `(let $id $args* := $val; $body) =>
    elabLetDeclAux stx id.getId args (mkHole stx) val body expectedType?
diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index bdbd51437f..4946c8e50e 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -94,14 +94,10 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> darrow >> termParser
 def letIdLhs      : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType
 def letSimpleDecl : Parser := try (letIdLhs >> " := ") >> termParser
 def letPatDecl    : Parser := termParser >> optType >> " := " >> termParser
-@[builtinTermParser] def «let» := parser! "let " >> (letSimpleDecl <|> letPatDecl) >> "; " >> termParser
-
-def equation            := matchAlt
-def letEqnsDecl : Parser := letIdLhs >> many1Indent equation "equations must be indented"
-@[builtinTermParser] def letEqns :=
-parser! "let " >> letEqnsDecl >> "; " >> termParser
-
-def letDecl := letSimpleDecl <|> letPatDecl <|> letEqnsDecl
+def equation               := matchAlt
+def letEqnsDecl   : Parser := letIdLhs >> many1Indent equation "equations must be indented"
+def letDecl                := letSimpleDecl <|> letPatDecl <|> letEqnsDecl
+@[builtinTermParser] def «let» := parser! "let " >> letDecl >> "; " >> termParser
 
 @[builtinTermParser] def «let_core» := parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser