From d54d759d56af1dc79829f97de6fa82eb8104cb6f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Feb 2018 13:51:16 -0800
Subject: [PATCH] refactor(library): do not use mk_fresh_name

---
 src/library/noncomputable.cpp | 2 +-
 src/library/quote.cpp         | 8 +++++++-
 src/library/util.cpp          | 6 +++---
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index f1402e9c0d..06ed9c14ee 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -166,7 +166,7 @@ struct get_noncomputable_reason_fn {
             expr e = _e;
             while (is_lambda(e) || is_pi(e)) {
                 expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-                expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
+                expr l = mk_local(m_tc.next_name(), binding_name(e), d, binding_info(e));
                 ls.push_back(l);
                 e = binding_body(e);
             }
diff --git a/src/library/quote.cpp b/src/library/quote.cpp
index 2b9fc20f3c..e394315566 100644
--- a/src/library/quote.cpp
+++ b/src/library/quote.cpp
@@ -120,13 +120,16 @@ expr const & get_antiquote_expr(expr const & e) {
     return get_annotation_arg(e);
 }
 
+static name * g_quote_fresh = nullptr;
+
 expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
     name x("_x");
+    name_generator ngen(*g_quote_fresh);
     buffer<expr> locals;
     buffer<expr> aqs;
     expr s = replace(e, [&](expr const & t, unsigned) {
             if (is_antiquote(t)) {
-                expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1),
+                expr local = mk_local(ngen.next(), x.append_after(locals.size() + 1),
                                       mk_expr_placeholder(), binder_info());
                 locals.push_back(local);
                 aqs.push_back(get_antiquote_expr(t));
@@ -147,6 +150,8 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
 }
 
 void initialize_quote() {
+    g_quote_fresh         = new name("_quote_fresh");
+    register_name_generator_prefix(*g_quote_fresh);
     g_expr_quote_macro    = new name("expr_quote_macro");
     g_expr_quote_opcode   = new std::string("Quote");
     g_expr           = new expr(mk_app(Const(get_expr_name()), mk_bool_tt()));
@@ -168,6 +173,7 @@ void initialize_quote() {
 }
 
 void finalize_quote() {
+    delete g_quote_fresh;
     delete g_expr_quote_pre;
     delete g_expr_quote_macro;
     delete g_expr_quote_opcode;
diff --git a/src/library/util.cpp b/src/library/util.cpp
index bc802d1f29..a30697ca32 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -232,7 +232,7 @@ bool is_reflexive_datatype(abstract_type_context & tc, name const & n) {
             if (is_pi(arg) && find(arg, [&](expr const & e, unsigned) { return is_constant(e) && const_name(e) == n; })) {
                 return true;
             }
-            expr local = mk_local(mk_fresh_name(), binding_domain(type));
+            expr local = mk_local(tc.next_name(), binding_domain(type));
             type = instantiate(binding_body(type), local);
         }
     }
@@ -429,9 +429,9 @@ expr to_telescope(type_checker & ctx, expr type, buffer<expr> & telescope, optio
         type = new_type;
         expr local;
         if (binfo)
-            local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), *binfo);
+            local = mk_local(ctx.next_name(), binding_name(type), binding_domain(type), *binfo);
         else
-            local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type));
+            local = mk_local(ctx.next_name(), binding_name(type), binding_domain(type), binding_info(type));
         telescope.push_back(local);
         type     = instantiate(binding_body(type), local);
         new_type = ctx.whnf(type);