From a57573a5b7ec451da4d426cc4c0e293e27831fca Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 12 Sep 2018 15:07:54 -0700
Subject: [PATCH] fix(library/init/lean/parser/command): keywords in notation
 actions are not actual keywords

---
 library/init/lean/parser/command.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 9f59b8b513..24babc0d63 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -81,9 +81,9 @@ node_choice! notation_symbol {
 def action.parser : command_parser :=
 node! action [":", action: node_choice! action_kind {
   prec: number,
-  "max",
-  "prev",
-  "scoped"
+  max: raw_symbol "max",
+  prev: raw_symbol "prev",
+  scoped: raw_symbol "scoped"
   /-TODO seq [
     "(",
     any_of ["foldl", "foldr"],