From 11e87545be3d7a6b2a77070deb768f01eaa8c5dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Feb 2018 13:36:16 -0800
Subject: [PATCH] chore(frontends/lean): remove dead variables

---
 src/frontends/lean/parser.cpp | 4 ----
 src/frontends/lean/pp.cpp     | 3 ---
 2 files changed, 7 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 71ee962eee..8faab1fcba 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -152,8 +152,6 @@ parser::error_if_undef_scope::error_if_undef_scope(parser & p):
 parser::all_id_local_scope::all_id_local_scope(parser & p):
     flet<id_behavior>(p.m_id_behavior, id_behavior::AllLocal) {}
 
-static name * g_tmp_prefix = nullptr;
-
 parser::parser(environment const & env, io_state const & ios,
                module_loader const & import_fn,
                std::istream & strm, std::string const & file_name,
@@ -2677,12 +2675,10 @@ void initialize_parser() {
     g_parser_show_errors     = new name{"parser", "show_errors"};
     register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
                          "(lean parser) display error messages in the regular output channel");
-    g_tmp_prefix = new name(name::mk_internal_unique_name());
 }
 
 void finalize_parser() {
     delete g_frontend_fresh;
-    delete g_tmp_prefix;
     delete g_parser_show_errors;
 }
 }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1a7154e041..1814168906 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -76,7 +76,6 @@ static format * g_visible_fmt     = nullptr;
 static format * g_show_fmt        = nullptr;
 static format * g_explicit_fmt    = nullptr;
 static format * g_partial_explicit_fmt    = nullptr;
-static name   * g_tmp_prefix      = nullptr;
 
 class nat_numeral_pp {
     name m_nat;
@@ -144,7 +143,6 @@ void initialize_pp() {
     g_show_fmt        = new format(highlight_keyword(format("show")));
     g_explicit_fmt    = new format(highlight_keyword(format("@")));
     g_partial_explicit_fmt    = new format(highlight_keyword(format("@@")));
-    g_tmp_prefix      = new name(name::mk_internal_unique_name());
     g_nat_numeral_pp  = new nat_numeral_pp();
 
     g_pp_using_anonymous_constructor = new name("pp_using_anonymous_constructor");
@@ -184,7 +182,6 @@ void finalize_pp() {
     delete g_show_fmt;
     delete g_partial_explicit_fmt;
     delete g_explicit_fmt;
-    delete g_tmp_prefix;
 }
 
 /** \brief We assume a metavariable name has a suggestion embedded in it WHEN its