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");