diff -r 965c24dd6856 -r d20cf282342e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Divides.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -2326,7 +2326,7 @@
   apply auto
 done
 
-declare TransferMorphism_nat_int [transfer add return:
+declare transfer_morphism_nat_int [transfer add return:
   transfer_nat_int_functions
   transfer_nat_int_function_closures
 ]
@@ -2341,7 +2341,7 @@
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
 
-declare TransferMorphism_int_nat [transfer add return:
+declare transfer_morphism_int_nat [transfer add return:
   transfer_int_nat_functions
   transfer_int_nat_function_closures
 ]