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;