diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index d5e155c1a..1780bb4c4 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -88,4 +88,8 @@ optional<expr> depends_on(unsigned sz, expr const * es, expr const & h) {
             return some_expr(es[i]);
     return none_expr();
 }
+
+bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs) {
+    return std::any_of(hs, hs+hs_sz, [&](expr const & h) { return depends_on(e, h); });
+}
 }
diff --git a/src/library/locals.h b/src/library/locals.h
index b0d1f8910..56ad9e1a0 100644
--- a/src/library/locals.h
+++ b/src/library/locals.h
@@ -40,4 +40,10 @@ inline bool depends_on(expr const & e, expr const & h) {
 
 /** \brief Return true iff one of \c es contains the local constant \c h */
 optional<expr> depends_on(unsigned sz, expr const * es, expr const & h);
+
+/** \brief Return true iff \c e depends on any of the local constants in \c hs */
+bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs);
+inline bool depends_on_any(expr const & e, buffer<expr> const & hs) {
+    return depends_on_any(e, hs.size(), hs.data());
+}
 }
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index bf420eafc..31e413f93 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -190,7 +190,7 @@ class inversion_tac {
         }
         if (!m_dep_elim) {
             expr const & g_type = g.get_type();
-            if (std::any_of(args.end() - m_nindices, args.end(), [&](expr const & arg) { return depends_on(g_type, arg); }))
+            if (depends_on_any(g_type, m_nindices, args.end() - m_nindices))
                 return false;
         }
         buffer<expr> hyps;
@@ -203,7 +203,7 @@ class inversion_tac {
                 continue;
             // h1 is not h nor any of the indices
             // Thus, it must not depend on the indices
-            if (std::any_of(args.end() - m_nindices, args.end(), [&](expr const & arg) { return depends_on(h1, arg); }))
+            if (depends_on_any(h1, m_nindices, args.end() - m_nindices))
                 return false;
         }
         return true;
@@ -216,7 +216,7 @@ class inversion_tac {
     void split_deps(buffer<expr> const & hyps, expr const & H, buffer<expr> & non_deps, buffer<expr> & deps, bool clear_H = false) {
         for (expr const & hyp : hyps) {
             expr const & hyp_type = mlocal_type(hyp);
-            if (depends_on(hyp_type, H) || std::any_of(deps.begin(), deps.end(), [&](expr const & dep) { return depends_on(hyp_type, dep); })) {
+            if (depends_on(hyp_type, H) || depends_on_any(hyp_type, deps)) {
                 deps.push_back(hyp);
             } else if (hyp != H || !clear_H) {
                 non_deps.push_back(hyp);