--- 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";