diff -r 21238c9d363e -r a129b817b58a src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/equalities.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -598,7 +598,7 @@
 qed "subset_iff_psubset_eq";
 
 goal thy "(!x. x ~: A) = (A={})";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "all_not_in_conv";
 AddIffs [all_not_in_conv];