From 96ea8b81c86089a3ce4c393ba9c0b7f079c72b98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Dec 2013 01:30:18 -0800
Subject: [PATCH] feat(frontends/lean/parser): change show-expression binder
 name

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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