diff -r bbcfeddeafbb -r 4da07afb065b src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Fri Apr 23 16:17:24 2010 +0200
+++ b/src/HOL/Library/Binomial.thy	Fri Apr 23 16:17:25 2010 +0200
@@ -391,13 +391,13 @@
   assumes kn: "k \<le> n" 
   shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
   using binomial_fact_lemma[OF kn]
-  by (simp add: field_simps of_nat_mult[symmetric])
+  by (simp add: field_eq_simps of_nat_mult [symmetric])
 
 lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
 proof-
   {assume kn: "k > n" 
     from kn binomial_eq_0[OF kn] have ?thesis 
-      by (simp add: gbinomial_pochhammer field_simps
+      by (simp add: gbinomial_pochhammer field_eq_simps
         pochhammer_of_nat_eq_0_iff)}
   moreover
   {assume "k=0" then have ?thesis by simp}
@@ -420,7 +420,7 @@
     from eq[symmetric]
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
-        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
+        gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
       apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult_assoc[symmetric] 
@@ -449,7 +449,7 @@
   have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
     unfolding gbinomial_pochhammer
     pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
-    by (simp add:  field_simps del: of_nat_Suc)
+    by (simp add:  field_eq_simps del: of_nat_Suc)
   also have "\<dots> = ?l" unfolding gbinomial_pochhammer
     by (simp add: ring_simps)
   finally show ?thesis ..