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;