diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index c6ec33a9d..da0a71ac3 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -144,36 +144,48 @@ void goal::get_hyps(buffer<expr> & r) const {
     get_app_args(m_meta, r);
 }
 
+static bool uses_name(name const & n, buffer<expr> const & locals) {
+    for (expr const & local : locals) {
+        if (is_local(local) && local_pp_name(local) == n)
+            return true;
+    }
+    return false;
+}
+
 name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & 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)
+        if (!uses_name(curr, locals))
             return curr;
     }
 }
 
 name get_unused_name(name const & prefix, buffer<expr> const & locals) {
+    if (!uses_name(prefix, locals))
+        return prefix;
     unsigned idx = 1;
     return get_unused_name(prefix, idx, locals);
 }
 
-name goal::get_unused_name(name const & prefix, unsigned & idx) const {
+name get_unused_name(name const & prefix, unsigned & idx, expr const & meta) {
     buffer<expr> locals;
-    get_app_rev_args(get_meta(), locals);
-    return ::lean::get_unused_name(prefix, idx, locals);
+    get_app_rev_args(meta, locals);
+    return get_unused_name(prefix, idx, locals);
+}
+
+name get_unused_name(name const & prefix, expr const & meta) {
+    buffer<expr> locals;
+    get_app_rev_args(meta, locals);
+    return get_unused_name(prefix, locals);
+}
+
+name goal::get_unused_name(name const & prefix, unsigned & idx) const {
+    return ::lean::get_unused_name(prefix, idx, m_meta);
 }
 
 name goal::get_unused_name(name const & prefix) const {
-    unsigned idx = 1;
-    return get_unused_name(prefix, idx);
+    return ::lean::get_unused_name(prefix, m_meta);
 }
 
 io_state_stream const & operator<<(io_state_stream const & out, goal const & g) {
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index 581c0d3f3..3bd06db2b 100644
--- a/src/library/tactic/goal.h
+++ b/src/library/tactic/goal.h
@@ -99,6 +99,8 @@ public:
 
 name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals);
 name get_unused_name(name const & prefix, buffer<expr> const & locals);
+name get_unused_name(name const & prefix, unsigned & idx, expr const & meta);
+name get_unused_name(name const & prefix, expr const & meta);
 
 io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
 
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index 9919b5757..325cfd588 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -40,7 +40,7 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
                     new_name = head(ns);
                     ns       = tail(ns);
                 } else {
-                    new_name = g.get_unused_name(binding_name(t));
+                    new_name = get_unused_name(binding_name(t), m);
                 }
                 expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t));
                 t              = instantiate(binding_body(t), new_local);