From f8fba6877b1d975bf1bc164af3370dd7bb11fc25 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 14 Jul 2019 08:19:42 -0700
Subject: [PATCH] fix(library/init/lean/parser/parser): add `ident` as possible
 first token for `symbolOrIdent`

---
 library/init/lean/parser/parser.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 367afa7d81..ab6c4054bb 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -815,7 +815,7 @@ fun c s =>
 symbolOrIdentFnAux sym ("expected '" ++ sym ++ "'")
 
 def symbolOrIdentInfo (sym : String) : ParserInfo :=
-{ firstTokens  := FirstTokens.tokens [ { val := sym, lbp := none } ] }
+{ firstTokens  := FirstTokens.tokens [ { val := sym }, { val := "ident" } ] }
 
 @[inline] def symbolOrIdent {k : ParserKind} (sym : String) : Parser k :=
 let sym := sym.trim;