src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Finite.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -257,7 +257,7 @@
    by (SELECT_GOAL Safe_tac 1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);
-  by (simp_tac (simpset() addsplits [expand_if]) 1);
+  by (Simp_tac 1);
   by (Blast_tac 1);
  by (dtac sym 1);
  by (rotate_tac ~1 1);
@@ -271,7 +271,7 @@
   by (SELECT_GOAL Safe_tac 1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
  by (Blast_tac 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
 by (SELECT_GOAL Safe_tac 1);
@@ -285,7 +285,7 @@
  by (SELECT_GOAL Safe_tac 1);
  by (res_inst_tac [("x","k")] exI 1);
  by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 val lemma = result();
 
@@ -341,9 +341,7 @@
 goal Finite.thy "!!A B. [| finite A; finite B |]\
 \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
 by (etac finite_induct 1);
-by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [Int_insert_left]
-	                    addsplits [expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
 qed_spec_mp "card_Un_disjoint";
 
 goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";