--- a/src/HOL/Induct/SList.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/SList.ML Fri Oct 17 15:25:12 1997 +0200
@@ -312,12 +312,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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
qed "mem_filter2";