src/HOL/Finite.ML
changeset 5477 41ab0f44dd8f
parent 5476 1c09934fe445
child 5516 d80e9aeb4a2b
--- a/src/HOL/Finite.ML	Fri Sep 11 12:55:40 1998 +0200
+++ b/src/HOL/Finite.ML	Fri Sep 11 14:09:46 1998 +0200
@@ -327,7 +327,8 @@
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
 by (fast_tac (claset() addss
-	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
+	      (simpset() addsimps [subset_insert_iff, finite_subset]
+			 delsimps [insert_subset])) 1);
 qed_spec_mp "card_mono";