diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index a8925776fd..638de8e0cf 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -67,9 +67,25 @@ static void tst3() {
     lean_assert(n == name(name(name("foo"), "bla"), "tst"));
 }
 
+static void tst4() {
+    lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla"}));
+    lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla", "foo"}));
+    lean_assert(is_prefix_of(name{"foo"}, name{"foo", "bla", "foo"}));
+    lean_assert(!is_prefix_of(name{"foo"}, name{"fo", "bla", "foo"}));
+    lean_assert(!is_prefix_of(name{"foo", "bla", "foo"}, name{"foo", "bla"}));
+    lean_assert(is_prefix_of(name{"foo", "bla"}, name(name{"foo", "bla"}, 0u)));
+    lean_assert(is_prefix_of(name(name(0u), 1u), name(name(0u), 1u)));
+    lean_assert(!is_prefix_of(name(name(0u), 3u), name(name(0u), 1u)));
+    lean_assert(is_prefix_of(name(name(0u), 1u), name(name(name(0u), 1u), "foo")));
+    lean_assert(!is_prefix_of(name(name(2u), 1u), name(name(name(0u), 1u), "foo")));
+    lean_assert(!is_prefix_of(name(name(0u), 3u), name(name(name(0u), 1u), "foo")));
+    lean_assert(!is_prefix_of(name(name("bla"), 1u), name(name(name(0u), 1u), "foo")));
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index d6315614ea..dd239cdc5c 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "name.h"
 #include "debug.h"
 #include "rc.h"
+#include "buffer.h"
 #include "hash.h"
 #include "trace.h"
 
@@ -66,7 +67,7 @@ struct name::imp {
             display_core(out, p);
     }
 
-    friend void copy_limbs(imp * p, std::vector<name::imp *> & limbs) {
+    friend void copy_limbs(imp * p, buffer<name::imp *> & limbs) {
         limbs.clear();
         while (p != nullptr) {
             limbs.push_back(p);
@@ -194,13 +195,41 @@ bool operator==(name const & a, name const & b) {
     }
 }
 
+bool is_prefix_of(name const & n1, name const & n2) {
+    buffer<name::imp*> limbs1, limbs2;
+    name::imp* i1 = n1.m_ptr;
+    name::imp* i2 = n2.m_ptr;
+    copy_limbs(i1, limbs1);
+    copy_limbs(i2, limbs2);
+    unsigned sz1 = limbs1.size();
+    unsigned sz2 = limbs2.size();
+    if (sz1 > sz2)
+        return false;
+    else if (sz1 == sz2 && n1.hash() != n2.hash())
+        return false;
+    auto it1 = limbs1.begin();
+    auto it2 = limbs2.begin();
+    for (; it1 != limbs1.end(); ++it1, ++it2) {
+        i1 = *it1;
+        i2 = *it2;
+        if (i1->m_is_string != i2->m_is_string)
+            return false;
+        if (i1->m_is_string) {
+            if (strcmp(i1->m_str, i2->m_str) != 0)
+                return false;
+        } else if (i1->m_k != i2->m_k) {
+            return false;
+        }
+    }
+    return true;
+}
+
 bool operator==(name const & a, char const * b) {
     return a.m_ptr->m_is_string && strcmp(a.m_ptr->m_str, b) == 0;
 }
 
 int cmp(name::imp * i1, name::imp * i2) {
-    static thread_local std::vector<name::imp *> limbs1;
-    static thread_local std::vector<name::imp *> limbs2;
+    buffer<name::imp *> limbs1, limbs2;
     copy_limbs(i1, limbs1);
     copy_limbs(i2, limbs2);
     auto it1 = limbs1.begin();
diff --git a/src/util/name.h b/src/util/name.h
index fdb5d57d06..968c1ad21f 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -31,6 +31,8 @@ public:
     static name const & anonymous();
     name & operator=(name const & other);
     name & operator=(name && other);
+    /** \brief Return true iff \c n1 is a prefix of \c n2. */
+    friend bool is_prefix_of(name const & n1, name const & n2);
     friend bool operator==(name const & a, name const & b);
     friend bool operator!=(name const & a, name const & b) { return !(a == b); }
     friend bool operator==(name const & a, char const * b);