src/HOLCF/Fix.ML

--- a/src/HOLCF/Fix.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Fix.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -889,7 +889,7 @@
 
 goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
 \           ==> adm (%x. P x = Q x)";
-by(subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
+by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
 by (Asm_simp_tac 1);
 by (rtac ext 1);
 by (fast_tac HOL_cs 1);