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