# HG changeset patch
# User paulson
# Date 868876948 -7200
# Node ID 2547f33fa33a6698c4d7f5d31b2f120b122c37ea
# Parent  4706267995116ea348d007784d683eb7a6304229
Removed redundant addsimps of Un_insert_left, which is now a default simprule

diff -r 470626799511 -r 2547f33fa33a src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jul 11 13:32:39 1997 +0200
+++ b/src/HOL/Finite.ML	Mon Jul 14 12:42:28 1997 +0200
@@ -59,7 +59,7 @@
 val major::prems = goal Finite.thy
     "[| finite F;  finite G |] ==> finite(F Un G)";
 by (rtac (major RS finite_induct) 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
 qed "finite_UnI";
 
 (*Every subset of a finite set is finite*)
@@ -332,8 +332,8 @@
 \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
 by (etac finite_induct 1);
 by (ALLGOALS 
-    (asm_simp_tac (!simpset addsimps [Un_insert_left, Int_insert_left]
-		            setloop split_tac [expand_if])));
+    (asm_simp_tac (!simpset addsimps [Int_insert_left]
+	                    setloop split_tac [expand_if])));
 qed_spec_mp "card_Un_disjoint";
 
 goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";