--- a/src/HOL/Relation.ML Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Relation.ML Wed Mar 06 12:52:11 1996 +0100
@@ -27,7 +27,7 @@
qed "idE";
goalw Relation.thy [id_def] "(a,b):id = (a=b)";
-by(fast_tac prod_cs 1);
+by (fast_tac prod_cs 1);
qed "pair_in_id_conv";