# HG changeset patch
# User wenzelm
# Date 963773971 -7200
# Node ID 2f06293f291aefe6c6b63c10f4d5ef337d2f7109
# Parent  cccba6147daedd6367b69e4291fa0851eba32fef
fixed nested prod syntax;

diff -r cccba6147dae -r 2f06293f291a src/HOL/Subst/Unify.ML
--- 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);