diff --git a/src/runtime/lean_obj.cpp b/src/runtime/lean_obj.cpp
index 6da0714401..a0ab3f9125 100644
--- a/src/runtime/lean_obj.cpp
+++ b/src/runtime/lean_obj.cpp
@@ -175,11 +175,11 @@ lean_obj * string_append(lean_obj * s1, lean_obj * s2) {
 lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2) {
     lean_assert(!is_scalar(a1) || !is_scalar(a2));
     if (is_scalar(a1))
-        return mk_mpz_core(unbox(a1) + mpz_value(a2));
+        return mk_nat_obj_core(unbox(a1) + mpz_value(a2));
     else if (is_scalar(a2))
-        return mk_mpz_core(mpz_value(a1) + unbox(a2));
+        return mk_nat_obj_core(mpz_value(a1) + unbox(a2));
     else
-        return mk_mpz_core(mpz_value(a1) + mpz_value(a2));
+        return mk_nat_obj_core(mpz_value(a1) + mpz_value(a2));
 }
 
 lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
@@ -189,23 +189,23 @@ lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
         return box(0);
     } else if (is_scalar(a2)) {
         lean_assert(mpz_value(a1) > unbox(a2));
-        return mk_mpz(mpz_value(a1) - unbox(a2));
+        return mk_nat_obj(mpz_value(a1) - unbox(a2));
     } else {
         if (mpz_value(a1) < mpz_value(a2))
             return box(0);
         else
-            return mk_mpz(mpz_value(a1) - mpz_value(a2));
+            return mk_nat_obj(mpz_value(a1) - mpz_value(a2));
     }
 }
 
 lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2) {
     lean_assert(!is_scalar(a1) || !is_scalar(a2));
     if (is_scalar(a1))
-        return mk_mpz_core(unbox(a1) * mpz_value(a2));
+        return mk_nat_obj_core(unbox(a1) * mpz_value(a2));
     else if (is_scalar(a2))
-        return mk_mpz_core(mpz_value(a1) * unbox(a2));
+        return mk_nat_obj_core(mpz_value(a1) * unbox(a2));
     else
-        return mk_mpz_core(mpz_value(a1) * mpz_value(a2));
+        return mk_nat_obj_core(mpz_value(a1) * mpz_value(a2));
 }
 
 lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
@@ -216,10 +216,10 @@ lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
         return box(0);
     } else if (is_scalar(a2)) {
         unsigned n2 = unbox(a2);
-        return n2 == 0 ? a2 : mk_mpz(mpz_value(a1) / n2);
+        return n2 == 0 ? a2 : mk_nat_obj(mpz_value(a1) / n2);
     } else {
         lean_assert(mpz_value(a2) != 0);
-        return mk_mpz(mpz_value(a1) / mpz_value(a2));
+        return mk_nat_obj(mpz_value(a1) / mpz_value(a2));
     }
 }
 
@@ -233,7 +233,7 @@ lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2) {
         return n2 == 0 ? a2 : box((mpz_value(a1) % mpz(n2)).get_unsigned_int());
     } else {
         lean_assert(mpz_value(a2) != 0);
-        return mk_mpz(mpz_value(a1) % mpz_value(a2));
+        return mk_nat_obj(mpz_value(a1) % mpz_value(a2));
     }
 }
 
@@ -267,31 +267,31 @@ bool nat_big_lt(lean_obj * a1, lean_obj * a2) {
 lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2) {
     lean_assert(!is_scalar(a1) || !is_scalar(a2));
     if (is_scalar(a1))
-        return mk_mpz(mpz(unbox(a1)) & mpz_value(a2));
+        return mk_nat_obj(mpz(unbox(a1)) & mpz_value(a2));
     else if (is_scalar(a2))
-        return mk_mpz(mpz_value(a1) & mpz(unbox(a2)));
+        return mk_nat_obj(mpz_value(a1) & mpz(unbox(a2)));
     else
-        return mk_mpz(mpz_value(a1) & mpz_value(a2));
+        return mk_nat_obj(mpz_value(a1) & mpz_value(a2));
 }
 
 lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2) {
     lean_assert(!is_scalar(a1) || !is_scalar(a2));
     if (is_scalar(a1))
-        return mk_mpz(mpz(unbox(a1)) | mpz_value(a2));
+        return mk_nat_obj(mpz(unbox(a1)) | mpz_value(a2));
     else if (is_scalar(a2))
-        return mk_mpz(mpz_value(a1) | mpz(unbox(a2)));
+        return mk_nat_obj(mpz_value(a1) | mpz(unbox(a2)));
     else
-        return mk_mpz(mpz_value(a1) | mpz_value(a2));
+        return mk_nat_obj(mpz_value(a1) | mpz_value(a2));
 }
 
 lean_obj * nat_big_lxor(lean_obj * a1, lean_obj * a2) {
     lean_assert(!is_scalar(a1) || !is_scalar(a2));
     if (is_scalar(a1))
-        return mk_mpz(mpz(unbox(a1)) ^ mpz_value(a2));
+        return mk_nat_obj(mpz(unbox(a1)) ^ mpz_value(a2));
     else if (is_scalar(a2))
-        return mk_mpz(mpz_value(a1) ^ mpz(unbox(a2)));
+        return mk_nat_obj(mpz_value(a1) ^ mpz(unbox(a2)));
     else
-        return mk_mpz(mpz_value(a1) ^ mpz_value(a2));
+        return mk_nat_obj(mpz_value(a1) ^ mpz_value(a2));
 }
 
 /* Debugging helper functions */
diff --git a/src/runtime/lean_obj.h b/src/runtime/lean_obj.h
index 9e07bf820a..a9bbfe0930 100644
--- a/src/runtime/lean_obj.h
+++ b/src/runtime/lean_obj.h
@@ -332,14 +332,14 @@ lean_obj * string_append(lean_obj * s1, lean_obj * s2);
 
 #define LEAN_MAX_SMALL_NAT (sizeof(void*) == 8 ? std::numeric_limits<unsigned>::max() : (std::numeric_limits<unsigned>::max() >> 1)) // NOLINT
 
-inline lean_obj * mk_mpz_core(mpz const & m) {
+inline lean_obj * mk_nat_obj_core(mpz const & m) {
     lean_assert(m > LEAN_MAX_SMALL_NAT);
     return alloc_mpz(m);
 }
 
-inline lean_obj * mk_mpz(mpz const & m) {
+inline lean_obj * mk_nat_obj(mpz const & m) {
     if (m > LEAN_MAX_SMALL_NAT)
-        return mk_mpz_core(m);
+        return mk_nat_obj_core(m);
     else
         return box(m.get_unsigned_int());
 }
@@ -350,15 +350,15 @@ inline lean_obj * mk_nat_obj(unsigned n) {
     } else if (n <= LEAN_MAX_SMALL_NAT) {
         return box(n);
     } else {
-        return mk_mpz_core(mpz(n));
+        return mk_nat_obj_core(mpz(n));
     }
 }
 
 inline lean_obj * mk_nat_obj(uint64 n) {
-    if (LEAN_LIKELY(n < LEAN_MAX_SMALL_NAT)) {
+    if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT)) {
         return box(n);
     } else {
-        return mk_mpz_core(mpz(n));
+        return mk_nat_obj_core(mpz(n));
     }
 }
 
@@ -371,7 +371,7 @@ inline lean_obj * nat_succ(lean_obj * a) {
     if (LEAN_LIKELY(is_scalar(a))) {
         return mk_nat_obj(nat2uint64(a) + 1);
     } else {
-        return mk_mpz_core(mpz_value(a) + 1);
+        return mk_nat_obj_core(mpz_value(a) + 1);
     }
 }