diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index f379031f14..1939ded882 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -61,9 +61,16 @@ static void tst2() {
     std::cout << "n1.hash(): " << n1.hash() << "\n";
 }
 
+static void tst3() {
+    name n{"foo", "bla", "tst"};
+    std::cout << n << "\n";
+    lean_assert(n == name(name(name("foo"), "bla"), "tst"));
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
     tst2();
+    tst3();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 4cb36e4188..96654704c6 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -124,6 +124,18 @@ name::name(name && other):m_ptr(other.m_ptr) {
     other.m_ptr = nullptr;
 }
 
+name::name(std::initializer_list<char const *> const & l):name() {
+    if (l.size() == 0) {
+        return;
+    } else {
+        auto it = l.begin();
+        *this = name(*it);
+        ++it;
+        for (; it != l.end(); ++it)
+            *this = name(*this, *it);
+    }
+}
+
 name::~name() {
     if (m_ptr)
         m_ptr->dec_ref();
diff --git a/src/util/name.h b/src/util/name.h
index ca4f6bfe16..29815f8525 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -28,6 +28,7 @@ public:
     name(name const & prefix, unsigned k);
     name(name const & other);
     name(name && other);
+    name(std::initializer_list<char const *> const & l);
     ~name();
     name & operator=(name const & other);
     name & operator=(name && other);