# HG changeset patch
# User nipkow
# Date 924192649 -7200
# Node ID f2a2a40e56c826126ca4a81a14cb5668ea05e21d
# Parent  228237ec56e50a49a9d2128206fa695217e96e6c
Proof mod.

diff -r 228237ec56e5 -r f2a2a40e56c8 src/HOL/ex/Qsort.ML
--- 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];