From 837915f06b5d4d5428df673100bb7765d995aab2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 1 Oct 2016 13:19:24 -0700
Subject: [PATCH] fix(frontends/lean/builtin_exprs): bug when parsing in quoted
 names

---
 src/frontends/lean/builtin_exprs.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 06b188eb68..c0a01d7ecc 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -591,7 +591,7 @@ static expr parse_quoted_name(parser & p, unsigned, expr const *, pos_info const
         if (p.curr_is_keyword() || p.curr_is_command()) {
             if (resolve)
                 throw parser_error("invalid resolved quote symbol, identifier is a keyword/command", pos);
-            id = p.get_name_val();
+            id = p.get_token_info().token();
             p.next();
         } else {
             id = p.check_id_next("invalid quoted name, identifier expected");