# HG changeset patch
# User wenzelm
# Date 1369402322 -7200
# Node ID 3fd0fe916097c6fb3aab81d0767d98338373e4c9
# Parent  7f3549a316f4d0f8fab913c88444d37a10be06a1
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

diff -r 7f3549a316f4 -r 3fd0fe916097 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri May 24 15:13:25 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 15:32:02 2013 +0200
@@ -239,7 +239,7 @@
 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
-         in unif thy ((name,Ts)::binders) (ts,tt) env end
+         in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
     | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
     | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
     | p => cases thy (binders,env,p)