Proof mod.

--- a/src/HOL/ex/Qsort.ML	Thu Apr 15 18:10:37 1999 +0200
+++ b/src/HOL/ex/Qsort.ML	Thu Apr 15 18:10:49 1999 +0200
@@ -37,7 +37,7 @@
 goal List.thy
   "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
 by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_full_simp_tac);
 qed"Ball_set_filter";
 Addsimps [Ball_set_filter];