diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Induct/Multiset0.ML
--- a/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -7,5 +7,5 @@
 *)
 
 Goal "(%x.0) : {f. finite {x. 0 < f x}}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "multiset_witness";