--- a/src/HOL/Set.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Set.ML Tue Dec 16 17:58:03 1997 +0100
@@ -452,7 +452,7 @@
AddSEs [singletonE];
goal Set.thy "{x. x=a} = {a}";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "singleton_conv";
Addsimps [singleton_conv];