Removal of card_insert_disjoint, which is now a default rewrite rule

--- a/src/HOL/Induct/Mutil.ML	Tue May 27 13:24:15 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue May 27 13:25:00 1997 +0200
@@ -141,8 +141,7 @@
 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
                                      tiling_domino_finite,
-                                     evnodd_subset RS finite_subset,
-                                     card_insert_disjoint]) 1);
+                                     evnodd_subset RS finite_subset]) 1);
 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
 qed "tiling_domino_0_1";