diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b5a1a477a..7d3e8326f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1385,7 +1385,7 @@ class parser::imp { if (curr_is_comma()) { next(); expr b = parse_expr(); - return mk_let("H", t, b, Var(0)); + return mk_let("show-expression", t, b, Var(0)); } else { check_next(scanner::token::By, "invalid 'show' expression, 'by' or ',' expected"); tactic tac = parse_tactic_expr();