# HG changeset patch
# User nipkow
# Date 889284569 -3600
# Node ID 74a12e86b20bd9c3d70e60dd8f1179c737c4b991
# Parent  9259feeeb2c88d5562b7e18450dad27885dd19f4
Removed `addsplits [expand_if]'

diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Arith.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -433,12 +433,11 @@
 qed "less_imp_diff_positive";
 
 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
-                       addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
 qed "if_Suc_diff_n";
 
 goal Arith.thy "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
 qed "diff_Suc_le_Suc_diff";
 
 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Event.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -46,22 +46,20 @@
 qed "spies_subset_spies_Says";
 
 goal thy "spies evs <= spies (Notes A X # evs)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Fast_tac 1);
 qed "spies_subset_spies_Notes";
 
 (*Spy sees all traffic*)
 goal thy "Says A B X : set evs --> X : spies evs";
 by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
-	      (simpset() addsplits [expand_event_case, expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
 qed_spec_mp "Says_imp_spies";
 
 (*Spy sees Notes of bad agents*)
 goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
 by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
-	      (simpset() addsplits [expand_event_case, expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
 qed_spec_mp "Notes_imp_spies";
 
 (*Use with addSEs to derive contradictions from old Says events containing
@@ -80,7 +78,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [parts_insert_spies]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 by (ALLGOALS Blast_tac);
 qed "parts_spies_subset_used";
 
@@ -91,7 +89,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [parts_insert_spies]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 by (ALLGOALS Blast_tac);
 bind_thm ("initState_into_used", impOfSubs (result()));
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Message.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -896,7 +896,7 @@
        (REPEAT o CHANGED)
            (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
-       simp_tac (simpset() addsplits [expand_if]) 1,
+       Simp_tac 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE 
          (Fake_insert_simp_tac 1
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -116,9 +116,9 @@
 
 
 (*Tactic for proving secrecy theorems*)
-fun analz_induct_tac i = 
+fun analz_induct_tac i =
     etac ns_public.induct i   THEN
-    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+    ALLGOALS Asm_simp_tac;
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -122,7 +122,7 @@
 (*Tactic for proving secrecy theorems*)
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
-    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+    ALLGOALS Asm_simp_tac;
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Public.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -76,7 +76,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [imageI, spies_Cons]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 qed_spec_mp "spies_pubK";
 
 (*Spy sees private keys of bad agents!*)
@@ -84,7 +84,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [imageI, spies_Cons]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 qed "Spy_spies_bad";
 
 AddIffs [spies_pubK, spies_pubK RS analz.Inj];
@@ -132,7 +132,7 @@
 by (res_inst_tac [("x","0")] exI 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [used_Cons]
-			addsplits [expand_event_case, expand_if])));
+			addsplits [expand_event_case])));
 by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
@@ -177,6 +177,5 @@
               addsimps [image_insert RS sym, image_Un RS sym,
 			rangeI, 
 			insert_Key_singleton, 
-			insert_Key_image, Un_assoc RS sym]
-              addsplits [expand_if];
+			insert_Key_image, Un_assoc RS sym];
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Shared.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -51,7 +51,7 @@
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [imageI, spies_Cons]
-	                addsplits [expand_event_case, expand_if])));
+	                addsplits [expand_event_case])));
 qed "Spy_spies_bad";
 
 AddSIs [Spy_spies_bad];
@@ -125,7 +125,7 @@
 by (res_inst_tac [("x","0")] exI 1);
 by (ALLGOALS (asm_simp_tac
 	      (simpset() addsimps [used_Cons]
-			addsplits [expand_event_case, expand_if])));
+			addsplits [expand_event_case])));
 by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
@@ -246,8 +246,7 @@
                          analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
                          insert_Key_singleton, subset_Compl_range,
                          Key_not_used, insert_Key_image, Un_assoc RS sym]
-                        @disj_comms)
-              addsplits [expand_if];
+                        @disj_comms);
 
 (*Lemma for the trivial direction of the if-and-only-if*)
 goal thy  
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/TLS.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -145,7 +145,7 @@
     REPEAT (FIRSTGOAL analz_mono_contra_tac)
     THEN 
     fast_tac (claset() addss (simpset())) i THEN
-    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+    ALLGOALS Asm_simp_tac;
 
 
 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
@@ -193,14 +193,12 @@
     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
-                         addsimps (expand_ifs@pushes)
-                         addsplits [expand_if]))  THEN
+                         addsimps (expand_ifs@pushes)))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
     ALLGOALS (asm_simp_tac 
               (simpset() addcongs [if_weak_cong]
-			 addsimps [insert_absorb]
-                         addsplits [expand_if]));
+			 addsimps [insert_absorb]));
 
 
 (*** Properties of items found in Notes ***)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -216,8 +216,7 @@
 by (ALLGOALS
     (asm_simp_tac 
      (simpset() addsimps expand_ifs
-	        addsimps [analz_insert_eq, analz_insert_freshK]
-                addsplits [expand_if])));
+	        addsimps [analz_insert_eq, analz_insert_freshK])));
 (*Oops*)
 by (blast_tac (claset() addDs [unique_session_keys]) 3);
 (*YM3*)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Divides.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -229,7 +229,7 @@
 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by Safe_tac;
 qed "mod2_cases";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b 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)";
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/IMP/Hoare.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -61,13 +61,13 @@
 (*Not suitable for rewriting: LOOPS!*)
 goal Hoare.thy "wp (WHILE b DO c) Q s = \
 \                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 qed "wp_While_if";
 
 goal thy
   "wp (WHILE b DO c) Q s = \
 \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (rtac iffI 1);
  by (rtac weak_coinduct 1);
   by (etac CollectI 1);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Com.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -54,7 +54,7 @@
 
 goalw thy [assign_def] "s[s x/x] = s";
 by (rtac ext 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 qed "assign_triv";
 
 Addsimps [assign_same, assign_different, assign_triv];
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/LFilter.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -98,7 +98,7 @@
 Addsimps [find_LCons_seek];
 
 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 qed "find_LCons";
 
 
@@ -148,8 +148,7 @@
 
 goal thy "lfilter p (LCons x l) = \
 \         (if p x then LCons x (lfilter p l) else lfilter p l)";
-by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
-                            addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
 qed "lfilter_LCons";
 
 AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -193,7 +192,7 @@
 
 goal thy "lfilter p (lfilter p l) = lfilter p l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
 by Safe_tac;
 (*Cases: p x is true or false*)
 by (rtac (lfilter_cases RS disjE) 1);
@@ -250,7 +249,7 @@
 \              ==> l'' = LCons y l' --> \
 \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
 by (etac findRel.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
 qed_spec_mp "findRel_conj_lfilter";
 
@@ -291,7 +290,7 @@
 
 goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
 by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
 qed "lfilter_conj";
 
@@ -329,7 +328,7 @@
 
 goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
 by Safe_tac;
 by (case_tac "lmap f l : Domain (findRel p)" 1);
 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Mutil.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -92,7 +92,7 @@
 goalw thy [evnodd_def]
     "evnodd (insert (i,j) C) b = \
 \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "evnodd_insert";
 
@@ -107,8 +107,7 @@
 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
 by (REPEAT_FIRST assume_tac);
 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc] 
-                          addsplits [expand_if]) 1
+by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1
            THEN Blast_tac 1));
 qed "domino_singleton";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Perm.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -41,7 +41,7 @@
 goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
 by (etac perm.induct 1);
 by (Fast_tac 4);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 val perm_mem_lemma = result();
 
 bind_thm ("perm_mem", perm_mem_lemma RS mp);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/PropLog.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -141,9 +141,7 @@
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
 by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_Diff";
 
@@ -151,9 +149,7 @@
   we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
 goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
 by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_insert";
 
@@ -174,7 +170,7 @@
 
 goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
 by (PropLog.pl.induct_tac "p" 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed "hyps_subset";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/SList.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -317,12 +317,12 @@
 
 goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
 by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mem_append2";
 
 goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mem_filter2";
 
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Integ/Bin.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -100,8 +100,6 @@
 
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
 
-val if_ss = simpset() addsplits [expand_if];
-
 
 (**** integ_of_bin ****)
 
@@ -109,26 +107,26 @@
 qed_goal "integ_of_bin_norm_Bcons" Bin.thy
     "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
  (fn _ =>[(bin.induct_tac "w" 1),
-          (ALLGOALS(simp_tac if_ss)) ]);
+          (ALLGOALS Simp_tac) ]);
 
 qed_goal "integ_of_bin_succ" Bin.thy
     "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
  (fn _ =>[(rtac bin.induct 1),
           (ALLGOALS(asm_simp_tac 
-                    (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+                    (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
 
 qed_goal "integ_of_bin_pred" Bin.thy
     "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
  (fn _ =>[(rtac bin.induct 1),
           (ALLGOALS(asm_simp_tac
-                  (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+                  (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
 
 qed_goal "integ_of_bin_minus" Bin.thy
     "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
  (fn _ =>[(rtac bin.induct 1),
           (Simp_tac 1),
           (Simp_tac 1),
-          (asm_simp_tac (if_ss
+          (asm_simp_tac (simpset()
                          delsimps [pred_Plus,pred_Minus,pred_Bcons]
                          addsimps [integ_of_bin_succ,integ_of_bin_pred,
                                    zadd_assoc]) 1)]);
@@ -143,16 +141,16 @@
 goal Bin.thy
     "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (rtac allI 1);
 by (bin.induct_tac "w" 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
 by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 val integ_of_bin_add_lemma = result();
 
 goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
@@ -165,12 +163,12 @@
 
 goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
 by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
 by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
                                   zadd_ac)) 1);
 qed "integ_of_bin_mult";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lambda/Eta.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -50,7 +50,7 @@
 by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (simpset())) 2);
 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
-                      addsplits [expand_if,expand_nat_case]) 1);
+                      addsplits [expand_nat_case]) 1);
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
 qed "free_subst";
@@ -168,7 +168,7 @@
 
 goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
 by (dB.induct_tac "s" 1);
-  by (simp_tac (simpset() addsplits [expand_if]) 1);
+  by (Simp_tac 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
    by (etac nat_neqE 1);
     by (res_inst_tac [("x","Var nat")] exI 1);
@@ -179,7 +179,7 @@
    by (assume_tac 2);
   by (etac thin_rl 1);
   by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-    by (simp_tac (simpset() addsplits [expand_if]) 1);
+    by (Simp_tac 1);
     by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    by (Simp_tac 1);
   by (Simp_tac 1);
@@ -195,7 +195,7 @@
  by (etac exE 1);
  by (etac rev_mp 1);
  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-   by (simp_tac (simpset() addsplits [expand_if]) 1);
+   by (Simp_tac 1);
   by (Simp_tac 1);
   by (Blast_tac 1);
  by (Simp_tac 1);
@@ -209,7 +209,7 @@
 by (etac exE 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("dB","t")] dB_case_distinction 1);
-  by (simp_tac (simpset() addsplits [expand_if]) 1);
+  by (Simp_tac 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
 by (Blast_tac 1);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -46,6 +46,7 @@
 (*** subst and lift ***)
 
 fun addsplit ss = ss addsimps [subst_Var]
+                     delsplits [expand_if]
                      setloop (split_inside_tac [expand_if]);
 
 goal Lambda.thy "(Var k)[u/k] = u";
@@ -66,8 +67,7 @@
 goal Lambda.thy
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]
-                                    addSolver cut_trans_tac)));
+by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
@@ -76,7 +76,7 @@
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
-                                addsplits [expand_if,expand_nat_case]
+                                addsplits [expand_nat_case]
                                 addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
@@ -88,7 +88,6 @@
 \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
-                                addsplits [expand_if]
                                 addSolver cut_trans_tac)));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
@@ -96,7 +95,7 @@
 
 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
 by (dB.induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_full_simp_tac);
 qed "subst_lift";
 Addsimps [subst_lift];
 
@@ -106,7 +105,9 @@
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
-                addsplits [expand_if,expand_nat_case]
+                 delsplits [expand_if]
+                 addsplits [expand_nat_case]
+                 addloop ("if",split_inside_tac[expand_if])
                 addSolver cut_trans_tac)));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lex/AutoChopper.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -18,7 +18,7 @@
 goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 val accept_not_Nil = result() repeat_RS spec;
 Addsimps [accept_not_Nil];
 
@@ -27,7 +27,7 @@
 \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
 by (list.induct_tac "xs" 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (strip_tac 1);
 by (rtac conjI 1);
 by (Fast_tac 1);
@@ -53,17 +53,17 @@
 \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
 \    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+by (Asm_simp_tac 1);
 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by (rename_tac "vss lrst" 1);  
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
  by (hyp_subst_tac 1);
  by (Simp_tac 1);
  by (fast_tac (claset() addSDs [no_acc]) 1);
 by (hyp_subst_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 val step2_a = (result() repeat_RS spec) RS mp;
 
 
@@ -73,11 +73,11 @@
 \     (if acc_prefix A st xs \
 \      then ys ~= [] \
 \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
@@ -96,11 +96,11 @@
 \     (if acc_prefix A st xs                   \
 \      then ? g. ys=r@g & fin A (nexts A st g)  \
 \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
@@ -135,11 +135,11 @@
 \     (if acc_prefix A st xs       \
 \      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by (rename_tac "vss lrst" 1);  
 by (Asm_simp_tac 1);
@@ -164,7 +164,7 @@
 by (Simp_tac 1);
 by (rtac trans 1);
  by (etac step2_a 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 val step2_d = (result() repeat_RS spec) RS mp;
 
 Delsimps [split_paired_All];
@@ -174,11 +174,11 @@
 \  (if acc_prefix A st xs  \
 \   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
 \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
  by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by (rtac conjI 1);
@@ -225,18 +225,18 @@
 by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
  by (rtac mp 1);
   by (etac step2_b 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (rtac conjI 1);
  by (rtac mp 1);
   by (etac step2_c 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (rtac conjI 1);
- by (asm_simp_tac (simpset() addsimps [step2_a] addsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsimps [step2_a]) 1);
 by (rtac conjI 1);
  by (rtac mp 1);
   by (etac step2_d 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (rtac mp 1);
  by (etac step2_e 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 qed"auto_chopper_is_auto_chopper";
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Lex/Regset_of_auto.ML
--- a/src/HOL/Lex/Regset_of_auto.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lex/Regset_of_auto.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -23,15 +23,14 @@
 
 goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
 by (exhaust_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "butlast_empty";
 AddIffs [butlast_empty];
 
 goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
 by (induct_tac "xss" 1);
  by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
-                           addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps) 1);
 by (rtac conjI 1);
  by (Clarify_tac 1);
  by (rtac conjI 1);
@@ -91,7 +90,7 @@
 by (res_inst_tac[("x","a#pref")]exI 1);
 by (res_inst_tac[("x","mids")]exI 1);
 by (res_inst_tac[("x","suf")]exI 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 qed_spec_mp "decompose";
 
 goal thy "!i. length(trace A i xs) = length xs";
@@ -137,7 +136,7 @@
 \ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [insert_commute]) 1);
 qed "set_trace_conv";
 
 goal thy
@@ -157,8 +156,7 @@
  "!i j xs. xs : regset_of A i j k = \
 \          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
 by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong]
-                        addsplits [expand_if,split_list_case]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
 by (strip_tac 1);
 by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
 by (rtac iffI 1);
@@ -168,12 +166,10 @@
  by (Asm_full_simp_tac 1);
  by (subgoal_tac
       "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
-  by (asm_simp_tac (simpset() addsplits [expand_if]
-       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+  by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
  by (etac star.induct 1);
   by (Simp_tac 1);
- by (asm_full_simp_tac (simpset() addsplits [expand_if]
-       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
 by (case_tac "k : set(butlast(trace A i xs))" 1);
  by (rtac disjI1 2);
  by (blast_tac (claset() addIs [lemma]) 2);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/List.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -311,13 +311,13 @@
 
 goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mem_append";
 Addsimps[mem_append];
 
 goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mem_filter";
 Addsimps[mem_filter];
 
@@ -333,7 +333,7 @@
 
 goal thy "(x mem xs) = (x: set xs)";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "set_mem_eq";
 
@@ -368,7 +368,7 @@
 
 goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by(Blast_tac 1);
 qed "in_set_filter";
 Addsimps [in_set_filter];
@@ -392,7 +392,7 @@
 
 goal thy "list_all P xs = (!x. x mem xs --> P(x))";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "list_all_mem_conv";
 
@@ -403,7 +403,7 @@
 
 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
 by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "filter_append";
 Addsimps [filter_append];
 
@@ -421,7 +421,7 @@
 
 goal thy "length (filter P xs) <= length xs";
 by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "length_filter";
 
 
@@ -512,7 +512,7 @@
 (* case 0 *)
 by (Asm_full_simp_tac 1);
 (* case Suc x *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
@@ -565,42 +565,40 @@
 
 goal thy "last(xs@[x]) = x";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "last_snoc";
 Addsimps [last_snoc];
 
 goal thy "butlast(xs@[x]) = xs";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "butlast_snoc";
 Addsimps [butlast_snoc];
 
 goal thy "length(butlast xs) = length xs - 1";
-by(res_inst_tac [("xs","xs")] snoc_induct 1);
-by(ALLGOALS Asm_simp_tac);
+by (res_inst_tac [("xs","xs")] snoc_induct 1);
+by (ALLGOALS Asm_simp_tac);
 qed "length_butlast";
 Addsimps [length_butlast];
 
 goal thy
   "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
 by (induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "butlast_append";
 
 goal thy "x:set(butlast xs) --> x:set xs";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "in_set_butlastD";
 
 goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]
-                          addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
 by (blast_tac (claset() addDs [in_set_butlastD]) 1);
 qed "in_set_butlast_appendI1";
 
 goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]
-                          addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
 by (Clarify_tac 1);
 by (Full_simp_tac 1);
 qed "in_set_butlast_appendI2";
@@ -751,15 +749,13 @@
 
 goal thy "takeWhile P xs @ dropWhile P xs = xs";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed "takeWhile_dropWhile_id";
 Addsimps [takeWhile_dropWhile_id];
 
 goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 by (Blast_tac 1);
 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 Addsimps [takeWhile_append1];
@@ -767,16 +763,14 @@
 goal thy
   "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 Addsimps [takeWhile_append2];
 
 goal thy
   "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 by (Blast_tac 1);
 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 Addsimps [dropWhile_append1];
@@ -784,15 +778,13 @@
 goal thy
   "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 Addsimps [dropWhile_append2];
 
 goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp"set_take_whileD";
 
 qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
@@ -805,21 +797,18 @@
 goal thy "set(remdups xs) = set xs";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
-                                 addsplits [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
 qed "set_remdups";
 Addsimps [set_remdups];
 
 goal thy "nodups(remdups xs)";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed "nodups_remdups";
 
 goal thy "nodups xs --> nodups (filter P xs)";
 by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "nodups_filter";
 
 (** replicate **)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Map.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -21,7 +21,7 @@
 qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
 	(K [Asm_simp_tac 1]);
 qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
-	(K [rtac ext 1, asm_simp_tac (simpset() addsplits [expand_if]) 1]);
+	(K [rtac ext 1, Asm_simp_tac 1]);
 (*Addsimps [update_same, update_other, update_triv];*)
 
 section "++";
@@ -56,14 +56,14 @@
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (rtac ext 1);
-by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
 qed "map_of_append";
 Addsimps [map_of_append];
 
 goal thy "map_of xs k = Some y --> (k,y):set xs";
 by (list.induct_tac "xs" 1);
 by  (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by (split_all_tac 1);
 by (Simp_tac 1);
 qed_spec_mp "map_of_SomeD";
@@ -76,7 +76,7 @@
 Addsimps [dom_empty];
 
 goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "dom_update";
 Addsimps [dom_update];
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Generalize.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -45,8 +45,8 @@
 by (typ.induct_tac "t1" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (Fast_tac 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
@@ -97,7 +97,7 @@
 by (rename_tac "R" 1);
 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
 by (typ.induct_tac "t" 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "gen_bound_typ_instance";
 
@@ -107,7 +107,7 @@
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
 by (typ.induct_tac "t" 1);
- by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Asm_simp_tac 1);
  by (Fast_tac 1);
 by (Asm_simp_tac 1);
 qed "free_tv_subset_gen_le";
@@ -121,8 +121,8 @@
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (subgoal_tac "n <= n + nat" 1);
 by (forw_inst_tac [("t","A")] new_tv_le 1);
 by (assume_tac 1);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Instance.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -66,8 +66,8 @@
 by (rename_tac "S1 S2" 1);
 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
 by Safe_tac;
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (dres_inst_tac [("x","x")] bspec 1);
 by (assume_tac 1);
@@ -82,8 +82,8 @@
 goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
 \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
 by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (simpset() addsimps [leD] addsplits [expand_if]) 1);
-by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [leD]) 1);
+by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "subst_to_scheme_inverse";
 
@@ -96,9 +96,9 @@
 \        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
 \                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
 by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
+by (simp_tac (simpset() addsimps [leD]) 1);
 by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
+by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
 val aux2 = result () RS mp;
 
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/MiniML.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -82,7 +82,7 @@
 goalw thy [free_tv_subst,dom_def]
           "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \               free_tv A Un free_tv t";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Fast_tac 1);
 qed "dom_S'";
 
@@ -110,7 +110,7 @@
 \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
 \         {x. ? y. x = n + y}";
 by (typ.induct_tac "t1" 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Fast_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Type.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -352,7 +352,7 @@
 
 goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
 by (type_scheme.induct_tac "sch" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (strip_tac 1);
 by (Fast_tac 1);
 qed "free_tv_ML_scheme";
@@ -423,14 +423,14 @@
 goal thy
   "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
 by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
 goal thy
   "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
 by (type_scheme.induct_tac "sch" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "subst_te_new_type_scheme";
 Addsimps [subst_te_new_type_scheme];
 
@@ -547,13 +547,13 @@
 Addsimps [new_tv_not_free_tv];
 
 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by Safe_tac;
 by (trans_tac 1);
 qed "less_maxL";
 
 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
 val less_maxR = result();
 
@@ -586,11 +586,11 @@
 Addsimps [fresh_variable_type_schemes];
 
 goalw thy [max_def] "!!n::nat. n <= (max n n')";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 val le_maxL = result();
 
 goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
 val le_maxR = result();
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/W.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -18,7 +18,7 @@
         "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 (* case Abs e *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -58,7 +58,7 @@
 by (assume_tac 2);
 by (rtac add_le_mono 1);
 by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
+by (simp_tac (simpset() addsimps [max_def]) 1);
 by (strip_tac 1);
 by (rtac new_tv_le 1);
 by (mp_tac 2);
@@ -66,7 +66,7 @@
 by (assume_tac 2);
 by (rtac add_le_mono 1);
 by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
+by (simp_tac (simpset() addsimps [max_def]) 1);
 by (strip_tac 1);
 by (dtac not_leE 1);
 by (rtac less_or_eq_imp_le 1);
@@ -81,7 +81,7 @@
 \                 new_tv m S & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 by (strip_tac 1);
 by (dtac new_tv_nth_nat_A 1);
 by (assume_tac 1);
@@ -178,7 +178,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (simp_tac (simpset() addsimps
-    [free_tv_subst] addsplits [split_option_bind,expand_if]) 1);
+    [free_tv_subst] addsplits [split_option_bind]) 1);
 by (strip_tac 1);
 by (case_tac "v : free_tv (A!nat)" 1);
 by (Asm_full_simp_tac 1);
@@ -272,7 +272,7 @@
         "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (strip_tac 1);
 by (rtac has_type.VarI 1);
 by (Simp_tac 1);
@@ -396,7 +396,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
-by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (eresolve_tac has_type_casesE 1); 
 by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
 by (etac exE 1);
@@ -457,7 +457,7 @@
 by (case_tac "na:free_tv Sa" 2);
 (* n1 ~: free_tv S1 *)
 by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_simp_tac 3);
 (* na : free_tv Sa *)
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
@@ -465,7 +465,7 @@
 by (Asm_simp_tac 2); 
 by (case_tac "na:dom Sa" 2);
 (* na ~: dom Sa *)
-by (asm_full_simp_tac (simpset() addsimps [dom_def] addsplits [expand_if]) 3);
+by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
 (* na : dom Sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
@@ -476,8 +476,7 @@
 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
     (simpset() addsimps [cod_def,free_tv_subst])) 3);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst] 
-                                     addsplits [expand_if])) 2);
+by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
 by (Simp_tac 2);  
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
@@ -488,10 +487,10 @@
 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv Sa" 2);
 (* case na ~: free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_full_simp_tac 3);
 by (Fast_tac 3);
 (* case na : free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -527,9 +526,9 @@
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv Sa" 1);
 (* case na ~: free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
 (* case na : free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
     eq_subst_scheme_list_eq_free] addss ((simpset() addsimps 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Nat.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -15,7 +15,6 @@
 qed "min_0R";
 
 goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
-by (split_tac [expand_if] 1);
 by (Simp_tac 1);
 qed "min_Suc_Suc";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/NatDef.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -599,12 +599,12 @@
 (** max
 
 goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "le_max_iff_disj";
 
 goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "max_le_iff_conj";
 
@@ -612,12 +612,12 @@
 (** min **)
 
 goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "le_min_iff_conj";
 
 goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "min_le_iff_disj";
  **)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Ord.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -43,14 +43,12 @@
 (** min **)
 
 goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by (split_tac [expand_if] 1);
 by (Asm_simp_tac 1);
 qed "min_leastL";
 
 val prems = goalw thy [min_def]
  "(!!x::'a::order. least <= x) ==> min x least = least";
 by (cut_facts_tac prems 1);
-by (split_tac [expand_if] 1);
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "min_leastR";
@@ -65,25 +63,25 @@
 qed "linorder_less_linear";
 
 goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by(cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_max_iff_disj";
 
 goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by(cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "max_le_iff_conj";
 
 goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by(cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_min_iff_conj";
 
 goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by(cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "min_le_iff_disj";
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Set.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -664,7 +664,7 @@
 
 (*Not for Addsimps -- it can cause goals to blow up!*)
 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 qed "mem_if";
 
 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Subst.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -41,7 +41,7 @@
 qed "agreement";
 
 goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by (simp_tac (simpset() addsimps [agreement] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [agreement]) 1);
 qed_spec_mp"repl_invariance";
 
 val asms = goal Subst.thy 
@@ -111,7 +111,7 @@
 by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 by (alist_ind_tac "r" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "subst_comp";
 
 Addsimps [subst_comp];
@@ -130,7 +130,7 @@
 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
 by (rtac allI 1);
 by (induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_full_simp_tac);
 qed "Cons_trivial";
 
 
@@ -143,7 +143,7 @@
 
 goal Subst.thy  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
 by (alist_ind_tac "s" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "sdom_iff";
 
@@ -203,7 +203,7 @@
 
 goal Subst.thy "(M <| [(x, Var x)]) = M";
 by (induct_tac "M" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "id_subst_lemma";
 
 Addsimps [id_subst_lemma];
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Subst/Unifier.ML
--- a/src/HOL/Subst/Unifier.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Unifier.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -82,8 +82,7 @@
 
 goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
 by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
-				 empty_iff_all_not]
-                       addsplits [expand_if]) 1);
+				 empty_iff_all_not]) 1);
 by (Blast_tac 1);
 qed_spec_mp "Var_Idem";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Unify.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -153,8 +153,7 @@
 (* Apply induction *)
 by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
 by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)
-			    addsplits [expand_if])));
+    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
 (*Const-Const case*)
 by (simp_tac
     (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
@@ -207,7 +206,7 @@
 
 goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 (*Const-Const case*)
 by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
 (*Const-Var case*)
@@ -245,8 +244,7 @@
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-       (simpset() addsimps [Var_Idem] 
-	         addsplits [expand_if,split_option_case])));
+       (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
 (*Comb-Comb case*)
 by Safe_tac;
 by (REPEAT (dtac spec 1 THEN mp_tac 1));
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/I.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -144,7 +144,7 @@
 goal I.thy "!a m s. \
 \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
 by (expr.induct_tac "e" 1);
-  by (simp_tac (simpset() addsimps [app_subst_list] addsplits [expand_if]) 1);
+  by (simp_tac (simpset() addsimps [app_subst_list]) 1);
  by (Simp_tac 1);
  by (strip_tac 1);
  by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/Type.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -157,7 +157,7 @@
 goal thy
   "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
 by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
@@ -259,7 +259,7 @@
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
-by (fast_tac (set_cs addss(simpset() addsplits [expand_if])) 1);
+by (fast_tac (set_cs addss simpset()) 1);
 qed_spec_mp "ftv_mem_sub_ftv_list";
 Addsimps [ftv_mem_sub_ftv_list];
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/W.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -14,7 +14,7 @@
         "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 (* case Abs e *)
 by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
                         addsplits [expand_bind]) 1);
@@ -45,7 +45,7 @@
         "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (fast_tac (HOL_cs addss(simpset() addsplits [expand_if])) 1);
+by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Abs e *)
 by (simp_tac (simpset() addsplits [expand_bind]) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -91,8 +91,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 
-        addsimps [id_subst_def,new_tv_list,new_tv_subst] 
-        addsplits [expand_if])) 1);
+        addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
 (* case Abs e *)
 by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
     addsplits [expand_bind]) 1);
@@ -159,7 +158,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
-    addss (simpset() addsplits [expand_if])) 1);
+    addss simpset()) 1);
 
 (* case Abs e *)
 by (asm_full_simp_tac (simpset() addsimps
@@ -225,8 +224,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
-by (simp_tac (simpset() addcongs [conj_cong] 
-              addsplits [expand_if]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (eresolve_tac has_type_casesE 1); 
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1);
 by (res_inst_tac [("x","s'")] exI 1);
@@ -284,7 +282,7 @@
 by (case_tac "na:free_tv sa" 2);
 (* na ~: free_tv sa *)
 by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_simp_tac 3);
 (* na : free_tv sa *)
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
@@ -293,8 +291,7 @@
 by (case_tac "na:dom sa" 2);
 (* na ~: dom sa *)
 (** LEVEL 50 **)
-by (asm_full_simp_tac (simpset() addsimps [dom_def] 
-                       addsplits [expand_if]) 3);
+by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
 (* na : dom sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
@@ -305,8 +302,7 @@
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
               (simpset() addsimps [cod_def,free_tv_subst])) 3);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst] 
-                            addsplits [expand_if])) 2);
+by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
 
 (** LEVEL 60 **)
 by (Simp_tac 2);  
@@ -320,9 +316,9 @@
 by (case_tac "na: free_tv t - free_tv sa" 2);
 (** LEVEL 69 **)
 (* case na ~: free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_full_simp_tac 3);
 (* case na : free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -358,9 +354,9 @@
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv sa" 1);
 (* case na ~: free_tv t - free_tv sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
 (* case na : free_tv t - free_tv sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
                             eq_subst_tel_eq_free] 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/WF.ML
--- a/src/HOL/WF.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/WF.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -153,7 +153,7 @@
   H_cong to expose the equality*)
 goalw WF.thy [cut_def]
     "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
+by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
 qed "cuts_eq";
 
 goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
@@ -193,8 +193,7 @@
 and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
 by (cut_facts_tac prems 1);
 by (rtac ext 1);
-by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
-                              addsplits [expand_if]) 1);
+by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
 qed "is_recfun_cut";
 
 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/equalities.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -115,7 +115,7 @@
 goalw thy [image_def]
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
-by (split_tac [expand_if] 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "if_image_distrib";
 Addsimps[if_image_distrib];
@@ -275,13 +275,13 @@
 
 goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
 \                                      else        B Int C)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "Int_insert_left";
 
 goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
 \                                      else        A Int B)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "Int_insert_right";
 
@@ -612,7 +612,7 @@
 qed "Diff_insert2";
 
 goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "insert_Diff_if";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Fib.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -58,8 +58,7 @@
 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
 by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
-				       mod_less, mod_Suc]
-                             addsplits [expand_if])));
+				       mod_less, mod_Suc])));
 by (ALLGOALS
     (asm_full_simp_tac
      (simpset() addsimps (fib.rules @ add_ac @ mult_ac @
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/InSort.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -8,8 +8,7 @@
 
 goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
 by (list.induct_tac "xs" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_simp_tac);
 qed "mset_ins";
 Addsimps [mset_ins];
 
@@ -19,8 +18,7 @@
 qed "insort_permutes";
 
 goal thy "set(ins f x xs) = insert x (set xs)";
-by (asm_simp_tac (simpset() addsimps [set_via_mset]
-                           addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
 by (Fast_tac 1);
 qed "set_ins";
 Addsimps [set_ins];
@@ -28,7 +26,7 @@
 val prems = goalw InSort.thy [total_def,transf_def]
   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted_ins";
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Primes.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -36,7 +36,7 @@
 
 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
 by (rtac (gcd_eq RS trans) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed "gcd_less_0";
 Addsimps [gcd_0, gcd_less_0];
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Qsort.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -26,7 +26,7 @@
 
 goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "qsort_permutes";
 
 goal Qsort.thy "set(qsort le xs) = set xs";
@@ -37,7 +37,7 @@
 goal List.thy
   "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed"Ball_set_filter";
 Addsimps [Ball_set_filter];
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/Recdef.ML
--- a/src/HOL/ex/Recdef.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Recdef.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -13,7 +13,7 @@
 
 goal thy "(x mem qsort (ord,l)) = (x mem l)";
 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "qsort_mem_stable";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Sorting.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -8,20 +8,20 @@
 
 goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mset_append";
 
 goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
 \                     mset xs x";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 qed "mset_compl_add";
 
 Addsimps [mset_append, mset_compl_add];
 
 goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
 by (Fast_tac 1);
 qed "set_via_mset";
 
diff -r 9259feeeb2c8 -r 74a12e86b20b src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/set.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -81,7 +81,7 @@
 
 goalw Lfp.thy [image_def]
     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "range_if_then_else";