diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 1321a8c9a..f2312eb11 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -28,7 +28,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator_exception.h"
 
 namespace lean {
-static name g_choice_name(name(name(name(0u), "library"), "choice"));
+static name g_choice_name = name::mk_internal_unique_name();
 static expr g_choice = mk_constant(g_choice_name);
 static format g_assignment_fmt  = format(":=");
 static format g_unification_u_fmt = format("\u2248");
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 5c29ae1c0..b96a69acb 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -99,7 +99,7 @@ static unsigned g_level_cup_prec  = 5;
 // A name that can't be created by the user.
 // It is used as placeholder for parsing A -> B expressions which
 // are syntax sugar for (Pi (_ : A), B)
-static name g_unused(name(0u), "parser");
+static name g_unused = name::mk_internal_unique_name();
 
 /**
     \brief Actual implementation for the parser functional object
diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp
index f1466a97c..d65fe21f1 100644
--- a/src/library/context_to_lambda.cpp
+++ b/src/library/context_to_lambda.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "library/context_to_lambda.h"
 
 namespace lean {
-static expr g_fake = Const(name(name(0u), "context_to_lambda"));
+static expr g_fake = Const(name::mk_internal_unique_name());
 expr context_to_lambda(context::iterator it, context::iterator const & end, expr const & e) {
     if (it == end) {
         return e;
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index ae334cd1d..02479fc6c 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -141,7 +141,7 @@ void tst2() {
 
 expr mk_big(expr f, unsigned depth, unsigned val) {
     if (depth == 1)
-        return Const(name(val));
+        return Const(name(name("foo"), val));
     else
         return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
 }
diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp
index c137cea58..88c567b01 100644
--- a/src/tests/kernel/replace.cpp
+++ b/src/tests/kernel/replace.cpp
@@ -17,7 +17,7 @@ using namespace lean;
 
 expr mk_big(expr f, unsigned depth, unsigned val) {
     if (depth == 1)
-        return mk_constant(name(val));
+        return mk_constant(name(name("foo"), val));
     else
         return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
 }
@@ -25,7 +25,7 @@ expr mk_big(expr f, unsigned depth, unsigned val) {
 static void tst1() {
     expr f = Const("f");
     expr r = mk_big(f, 16, 0);
-    expr n = Const(name(0u));
+    expr n = Const(name("foo"));
     for (unsigned i = 0; i < 20; i++) {
         r = abstract(r, n);
     }
diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 0f42b00e5..0513cf461 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -13,7 +13,6 @@ using namespace lean;
 static void tst1() {
     name n("foo");
     lean_assert(n == name("foo"));
-    lean_assert(n != name(1));
     lean_assert(name(n, 1) != name(n, 2));
     lean_assert(name(n, 1) == name(n, 1));
     lean_assert(name(name(n, 1), 2) != name(name(n, 1), 1));
@@ -37,13 +36,6 @@ static void tst1() {
     lean_assert(name(n, 1) < name(n, "xxx"));
     lean_assert(name(n, 1) < name(name(n, "xxx"), 1));
     lean_assert(name() < name(name(n, "xxx"), 1));
-    lean_assert(name(1) < name(name(n, "xxx"), 1));
-    lean_assert(name(1) < name(2));
-    lean_assert(name(2) > name(1));
-    lean_assert(name(1) > name());
-    lean_assert(name(2) < name(name("foo"), 1));
-    lean_assert(name(0u) < name(name(1), "foo"));
-    lean_assert(name(2) > name(name(1), "foo"));
 }
 
 static name mk_big_name(unsigned num) {
@@ -76,24 +68,15 @@ static void tst4() {
     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")));
 }
 
 static void tst5() {
-    name n(0u);
-    lean_assert(n.size() == 1);
     lean_assert(name().size() > 0);
     lean_assert(name({"foo", "bla", "boing"}).get_prefix() == name({"foo", "bla"}));
     lean_assert(!name({"foo", "bla", "boing"}).is_atomic());
     lean_assert(name({"foo"}).is_atomic());
     lean_assert(strcmp(name({"foo", "bla", "boing"}).get_string(), "boing") == 0);
-    lean_assert(name(name(0u), 1u).get_numeral() == 1u);
-    lean_assert(name(2u).get_numeral() == 2u);
+    lean_assert(name(name("foo"), 1u).get_numeral() == 1u);
     lean_assert(name::anonymous().is_anonymous());
     name n1("foo");
     name n2 = n1;
@@ -101,30 +84,32 @@ static void tst5() {
     std::cout << name::anonymous() << "\n";
     std::cout << name({"foo", "bla", "boing"}).get_prefix() << "\n";
     lean_assert(name("foo").is_string());
-    lean_assert(name(0u).is_numeral());
-    lean_assert(name(name(0u), "foo").is_string());
+    lean_assert(name(name("boo"), "foo").is_string());
     lean_assert(name(name("foo"), 0u).is_numeral());
-    lean_assert(name(name(0u), "foo").get_prefix().is_numeral());
     lean_assert(name(name("foo"), 0u).get_prefix().is_string());
 }
 
 static void tst6() {
     lean_assert(name({"foo", "bla"}).is_safe_ascii());
-    lean_assert(name(123u).is_safe_ascii());
-    lean_assert(name(name(name(230u), "bla"), "foo").is_safe_ascii());
     lean_assert(!name({"foo", "b\u2200aaa"}).is_safe_ascii());
     lean_assert(!name({"\u2200", "boo"}).is_safe_ascii());
-    lean_assert(!name(name(name(230u), "bla\u2200"), "foo").is_safe_ascii());
+    lean_assert(!name(name(name("baa"), "bla\u2200"), "foo").is_safe_ascii());
 }
 
 static void tst7() {
     lean_assert(name("foo") + name("bla") == name({"foo", "bla"}));
     lean_assert(name("foo") + name({"bla", "test"}) == name({"foo", "bla", "test"}));
     lean_assert(name({"foo", "hello"}) + name({"bla", "test"}) == name({"foo", "hello", "bla", "test"}));
-    lean_assert(name("foo") + (name(10u) + name({"bla", "test"})) == name(name(name(name("foo"), 10u), "bla"), "test"));
+    lean_assert(name("foo") + (name("bla") + name({"bla", "test"})) == name(name(name(name("foo"), "bla"), "bla"), "test"));
     lean_assert(name() + name({"bla", "test"}) == name({"bla", "test"}));
     lean_assert(name({"bla", "test"}) + name() == name({"bla", "test"}));
-    lean_assert(name(10u) + name(20u) == name(name(10u), 20u));
+}
+
+static void tst8() {
+    name u1 = name::mk_internal_unique_name();
+    name u2 = name::mk_internal_unique_name();
+    lean_assert(u1 != u2);
+    std::cout << u1 << " " << u2 << "\n";
 }
 
 int main() {
@@ -135,5 +120,6 @@ int main() {
     tst5();
     tst6();
     tst7();
+    tst8();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 5240318df..6c02f6bc9 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <sstream>
 #include <string>
+#include <atomic>
 #include "util/name.h"
 #include "util/debug.h"
 #include "util/rc.h"
@@ -102,7 +103,7 @@ name::name(name const & prefix, char const * name) {
         m_ptr->m_hash = hash_str(sz, name, 0);
 }
 
-name::name(name const & prefix, unsigned k) {
+name::name(name const & prefix, unsigned k, bool) {
     m_ptr      = new imp(false, prefix.m_ptr);
     m_ptr->m_k = k;
     if (m_ptr->m_prefix)
@@ -111,10 +112,14 @@ name::name(name const & prefix, unsigned k) {
         m_ptr->m_hash = k;
 }
 
+name::name(name const & prefix, unsigned k):name(prefix, k, true) {
+    lean_assert(prefix.m_ptr);
+}
+
 name::name(char const * n):name(name(), n) {
 }
 
-name::name(unsigned k):name(name(), k) {
+name::name(unsigned k):name(name(), k, true) {
 }
 
 name::name(name const & other):m_ptr(other.m_ptr) {
@@ -150,6 +155,13 @@ name const & name::anonymous() {
     return g_anonymous;
 }
 
+static std::atomic<unsigned> g_next_id(0);
+
+name name::mk_internal_unique_name() {
+    unsigned id = std::atomic_fetch_add(&g_next_id, 1u);
+    return name(id);
+}
+
 name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); }
 
 name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); }
diff --git a/src/util/name.h b/src/util/name.h
index 75c0a359f..6b9f24d90 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -19,10 +19,12 @@ class name {
     friend int cmp(imp * i1, imp * i2);
     imp * m_ptr;
     explicit name(imp * p);
+    explicit name(unsigned k);
+    // the parameter bool is only used to distinguish this constructor from the public one.
+    name(name const & prefix, unsigned k, bool);
 public:
     name();
     name(char const * name);
-    explicit name(unsigned k);
     name(name const & prefix, char const * name);
     name(name const & prefix, unsigned k);
     name(name const & other);
@@ -35,6 +37,20 @@ public:
     name(std::initializer_list<char const *> const & l);
     ~name();
     static name const & anonymous();
+    /**
+        \brief Create a unique internal name that is not meant to exposed
+        to the user. Different modules require a unique name.
+        The unique name is created using a numeric prefix.
+        A module that needs to create several unique names should
+        the following idiom:
+        <code>
+            name unique_prefix = name::mk_internal_unique_name();
+            name unique_name_1(unique_prefix, 1);
+            ...
+            name unique_name_k(unique_prefix, k);
+        </code>
+    */
+    static name mk_internal_unique_name();
     name & operator=(name const & other);
     name & operator=(name && other);
     /** \brief Return true iff \c n1 is a prefix of \c n2. */