diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -253,12 +253,7 @@
 lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
   card (A <*> B) = card(A) * card(B)";
   apply (rule_tac F = A in finite_induct, auto)
-  apply (case_tac "F = {}", force)
-  apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) + 
-    card(F <*> B)");
-  apply simp
-  apply (rule card_Un_disjoint)
-  by auto
+  done
 
 (******************************************************************)
 (*                                                                *)