From da04491df1d44eeebf7c1ccc0e3135310b8e5818 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 2 Oct 2018 09:16:24 -0700
Subject: [PATCH] fix(frontends/lean/builtin_exprs): trim view field names

---
 src/frontends/lean/builtin_exprs.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 7e23dda401..205d3e1c2c 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -892,7 +892,7 @@ static expr parse_node(parser & p, unsigned, expr const *, pos_info const &) {
             name fname;
             expr reader;
             if (p.curr_is_string()) {
-                fname = p.get_str_val();
+                fname = utf8_trim(p.get_str_val());
                 p.next();
                 reader = mk_app(mk_const({"lean", "parser", "symbol"}), from_string(p.get_str_val()));
                 if (p.curr_is_token(":")) {
@@ -934,7 +934,7 @@ static expr parse_choice(parser & p, unsigned, expr const *, pos_info const &) {
         name fname;
         expr reader;
         if (p.curr_is_string()) {
-            fname = p.get_str_val();
+            fname = utf8_trim(p.get_str_val());
             p.next();
             reader = mk_app(mk_const({"lean", "parser", "symbol"}), from_string(p.get_str_val()));
             if (p.curr_is_token(":")) {