src/HOL/ZF/HOLZF.thy

 lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n"
   by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat])
 
 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   apply (simp add: Nat2nat_def)
-  apply (rule_tac f_inv_onto_f)
+  apply (rule_tac f_inv_into_f)
   apply (auto simp add: image_def Nat_def Sep)
   done
 
 lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)"
   apply (auto simp add: Nat_def Sep Nat2nat_def)