--- a/src/HOL/Number_Theory/Cong.thy Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Cong.thy Mon Mar 08 09:38:58 2010 +0100
@@ -131,7 +131,7 @@
apply assumption
done
-declare TransferMorphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_cong]
lemma transfer_int_nat_cong:
@@ -140,7 +140,7 @@
apply (auto simp add: zmod_int [symmetric])
done
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_cong]