ex/qsort.ML

--- a/ex/qsort.ML	Tue Mar 22 19:55:29 1994 +0100
+++ b/ex/qsort.ML	Sun Mar 27 12:36:39 1994 +0200
@@ -6,8 +6,7 @@
 Two verifications of Quicksort
 *)
 
-val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons]
-                    delsimps [conj_assoc] addsimps conj_ac;
+val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
 
 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);