diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Qsort.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -35,7 +35,7 @@
 Addsimps [set_qsort];
 
 goal List.thy
-  "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
+  "(!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 setloop (split_tac [expand_if]))));
 qed"Ball_set_filter";