src/HOL/Number_Theory/Primes.thy

 lemma transfer_nat_int_prime:
   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
   unfolding gcd_int_def lcm_int_def prime_int_def
   by auto
 
-declare TransferMorphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_prime]
 
 lemma transfer_int_nat_prime:
   "prime (int x) = prime x"
   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
 
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_prime]
 
 
 subsection {* Primes *}