diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 1ca173c13..bf6955508 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -209,7 +209,7 @@ _
 
 irreducible int
 definition of_nat [coercion] [reducible] (n : ℕ) : ℤ := psub (pair n 0)
-definition of_num [coercion] [reducible] (n : num) : ℤ := of_nat (nat.to_nat n)
+definition of_num [coercion] [reducible] (n : num) : ℤ := of_nat (nat.of_num n)
 
 theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
 have H : rel (pair n n) (pair 0 0), by simp,
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index b7be6ba6f..01d4e1af3 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -47,7 +47,7 @@ definition add (x y : ℕ) : ℕ :=
 nat.rec x (λ n r, succ r) y
 infixl `+` := add
 
-definition to_nat [coercion] [reducible] (n : num) : ℕ :=
+definition of_num [coercion] [reducible] (n : num) : ℕ :=
 num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n