diff -r 3167079f4cd1 -r 1bdaa24fb56d src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Thu Mar 11 15:52:34 2010 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Thu Mar 11 15:52:35 2010 +0100
@@ -364,7 +364,7 @@
         finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
           card F choose (k + 1) + (card F choose k)".
         with iassms choose_plus_one_nat show ?thesis
-          by auto
+          by (auto simp del: card.insert)
       qed
     qed
   qed