diff --git a/src/util/name.cpp b/src/util/name.cpp
index ac237ce151..47ba946011 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -111,15 +111,6 @@ name::name(char const * n):name(name(), n) {
 name::name(unsigned k):name(name(), k, true) {
 }
 
-name::name(name const & other):m_ptr(other.m_ptr) {
-    if (m_ptr)
-        m_ptr->inc_ref();
-}
-
-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;
@@ -132,11 +123,6 @@ name::name(std::initializer_list<char const *> const & l):name() {
     }
 }
 
-name::~name() {
-    if (m_ptr)
-        m_ptr->dec_ref();
-}
-
 static name * g_anonymous = nullptr;
 
 name const & name::anonymous() {
@@ -162,16 +148,6 @@ name_kind name::kind() const {
         return m_ptr->m_is_string ? name_kind::STRING : name_kind::NUMERAL;
 }
 
-unsigned name::get_numeral() const {
-    lean_assert(is_numeral());
-    return m_ptr->m_k;
-}
-
-char const * name::get_string() const {
-    lean_assert(is_string());
-    return m_ptr->m_str;
-}
-
 /* Equality test core procedure, it is invoked by operator== */
 bool eq_core(name::imp * i1, name::imp * i2) {
     while (true) {
@@ -260,14 +236,6 @@ int cmp(name::imp * i1, name::imp * i2) {
     else return it1 == limbs1.end() ? -1 : 1;
 }
 
-bool name::is_atomic() const {
-    return m_ptr == nullptr || m_ptr->m_prefix == nullptr;
-}
-
-name name::get_prefix() const {
-    return is_atomic() ? name() : name(m_ptr->m_prefix);
-}
-
 static unsigned num_digits(unsigned k) {
     if (k == 0)
         return 1;
diff --git a/src/util/name.h b/src/util/name.h
index 4e0e13faa4..55908be5d9 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -57,15 +57,15 @@ public:
     name(std::string const & s):name(s.c_str()) {}
     name(name const & prefix, char const * name);
     name(name const & prefix, unsigned k);
-    name(name const & other);
-    name(name && other);
+    name(name const & other):m_ptr(other.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    name(name && other):m_ptr(other.m_ptr) { other.m_ptr = nullptr; }
     /**
        \brief Create a hierarchical name using the given strings.
        Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
        name <tt>foo::bla::tst</tt>.
     */
     name(std::initializer_list<char const *> const & l);
-    ~name();
+    ~name() { if (m_ptr) m_ptr->dec_ref(); }
     static name const & anonymous();
     /**
         \brief Create a unique internal name that is not meant to exposed
@@ -107,22 +107,22 @@ public:
     friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; }
     friend bool operator>=(name const & a, name const & b) { return cmp(a, b) >= 0; }
     name_kind kind() const;
-    bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; }
-    bool is_string() const    { return kind() == name_kind::STRING; }
-    bool is_numeral() const   { return kind() == name_kind::NUMERAL; }
-    explicit operator bool() const     { return !is_anonymous(); }
-    unsigned get_numeral() const;
+    bool is_anonymous() const { return m_ptr == nullptr; }
+    bool is_string() const    { return m_ptr != nullptr && m_ptr->m_is_string; }
+    bool is_numeral() const   { return m_ptr != nullptr && !m_ptr->m_is_string; }
+    explicit operator bool() const { return m_ptr != nullptr; }
+    unsigned get_numeral() const { lean_assert(is_numeral()); return m_ptr->m_k; }
     /**
        \brief If the tail of the given hierarchical name is a string, then it returns this string.
        \pre is_string()
     */
-    char const * get_string() const;
-    bool is_atomic() const;
+    char const * get_string() const { lean_assert(is_string()); return m_ptr->m_str; }
+    bool is_atomic() const { return m_ptr == nullptr || m_ptr->m_prefix == nullptr; }
     /**
         \brief Return the prefix of a hierarchical name
         \pre !is_atomic()
     */
-    name get_prefix() const;
+    name get_prefix() const { return is_atomic() ? name() : name(m_ptr->m_prefix); }
     /** \brief Convert this hierarchical name into a string. */
     std::string to_string(char const * sep = lean_name_separator) const;
     /** \brief Size of the this name (in characters). */