src/HOL/Set.ML

--- a/src/HOL/Set.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -311,7 +311,7 @@
     (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
 
 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
-by(fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
+by (fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
 qed "singletonD";
 
 val singletonE = make_elim singletonD;