src/HOL/WF.ML

--- a/src/HOL/WF.ML	Thu Jun 10 10:41:36 1999 +0200
+++ b/src/HOL/WF.ML	Thu Jun 10 10:50:19 1999 +0200
@@ -236,7 +236,7 @@
 qed "acyclic_converse";
 
 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
-by(blast_tac (claset() addIs [trancl_mono]) 1);
+by (blast_tac (claset() addIs [trancl_mono]) 1);
 qed "acyclic_subset";
 
 (** cut **)