From a311f05add5de68e286b97fb4f082c3a84edc5ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Nov 2014 18:46:08 -0800
Subject: [PATCH] refactor(library/tactic): move 'get_unused_name' to goal

---
 src/library/tactic/goal.cpp          | 23 +++++++++++++++++++++++
 src/library/tactic/goal.h            |  5 +++++
 src/library/tactic/intros_tactic.cpp | 21 +--------------------
 3 files changed, 29 insertions(+), 20 deletions(-)

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index c46ec4d06d..7b009c7e47 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -144,6 +144,29 @@ void goal::get_hyps(buffer<expr> & r) const {
     get_app_args(m_meta, r);
 }
 
+name goal::get_unused_name(name const & prefix, unsigned & idx) const {
+    buffer<expr> locals;
+    get_app_rev_args(get_meta(), locals);
+    while (true) {
+        bool used = false;
+        name curr = prefix.append_after(idx);
+        idx++;
+        for (expr const & local : locals) {
+            if (is_local(local) && local_pp_name(local) == curr) {
+                used = true;
+                break;
+            }
+        }
+        if (!used)
+            return curr;
+    }
+}
+
+name goal::get_unused_name(name const & prefix) const {
+    unsigned idx = 1;
+    return get_unused_name(prefix, idx);
+}
+
 io_state_stream const & operator<<(io_state_stream const & out, goal const & g) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(g.pp(out.get_formatter()), opts);
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index f6748b1c5b..a643c1020b 100644
--- a/src/library/tactic/goal.h
+++ b/src/library/tactic/goal.h
@@ -88,6 +88,11 @@ public:
     */
     void get_hyps(buffer<expr> & r) const;
 
+    /** \brief Return a "user" name that is not used by any local constant in the given goal */
+    name get_unused_name(name const & prefix, unsigned & idx) const;
+
+    name get_unused_name(name const & prefix) const;
+
     format pp(formatter const & fmt, substitution const & s) const;
     format pp(formatter const & fmt) const;
 };
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index 6c2362f7ce..2983574bde 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -10,25 +10,6 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-/** \brief Return a "user" name that is not used by any local constant in the given goal */
-static name get_unused_name(goal const & g, name const & prefix, unsigned & idx) {
-    buffer<expr> locals;
-    get_app_rev_args(g.get_meta(), locals);
-    while (true) {
-        bool used = false;
-        name curr = prefix.append_after(idx);
-        idx++;
-        for (expr const & local : locals) {
-            if (is_local(local) && local_pp_name(local) == curr) {
-                used = true;
-                break;
-            }
-        }
-        if (!used)
-            return curr;
-    }
-}
-
 tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
     auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
         list<name> ns    = _ns;
@@ -60,7 +41,7 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
                     new_name = head(ns);
                     ns       = tail(ns);
                 } else {
-                    new_name = get_unused_name(g, name("H"), nidx);
+                    new_name = g.get_unused_name(name("H"), nidx);
                 }
                 expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t));
                 t              = instantiate(binding_body(t), new_local);