fixed nested prod syntax;

--- a/src/HOL/Subst/Unify.ML	Sun Jul 16 20:59:06 2000 +0200
+++ b/src/HOL/Subst/Unify.ML	Sun Jul 16 20:59:31 2000 +0200
@@ -145,7 +145,7 @@
  *---------------------------------------------------------------------------*)
 by (subgoal_tac "!M1 M2 theta.  \
  \   unify(M1, M2) = Some theta --> \
- \   (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1);
+ \   (!N1 N2. ((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)" 1);
 by (Blast_tac 1);
 by (rtac allI 1); 
 by (rtac allI 1);