diff -r 424c7b1489df -r 64eda8afe2b4 ex/Qsort.ML
--- a/ex/Qsort.ML	Tue Feb 15 07:55:22 1994 +0100
+++ b/ex/Qsort.ML	Tue Feb 15 10:05:17 1994 +0100
@@ -84,11 +84,6 @@
   Qsort.qsort_Nil,Qsort.qsort_Cons];
 
 
-goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
-
 goal Qsort.thy "x mem qsort(le,xs)  =  x mem xs";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));