--- a/src/HOL/Number_Theory/Binomial.thy Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Binomial.thy Mon Mar 08 09:38:58 2010 +0100
@@ -73,7 +73,7 @@
"n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
by (auto simp add: binomial_int_def)
-declare TransferMorphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_binomial transfer_nat_int_binomial_closure]
lemma transfer_int_nat_binomial:
@@ -84,7 +84,7 @@
"is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
by (auto simp add: binomial_int_def)
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_binomial transfer_int_nat_binomial_closure]