src/Pure/pattern.ML

     | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
     | p => cases thy (binders,env,p)
 
 and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
        ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
-         if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
-                  else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
+          if F = G then
+            let val env' = unify_types thy (Fty, Gty) env
+            in flexflex1(env',binders,F,Fty,ints_of' env' ss,ints_of' env' ts) end
+          else
+            let val env' =
+              unify_types thy
+               (Envir.body_type env (length ss) Fty,
+                Envir.body_type env (length ts) Gty) env
+            in flexflex2(env',binders,F,Fty,ints_of' env' ss,G,Gty,ints_of' env' ts) end
       | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
       | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
       | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
       | ((Free(f),ss),(Free(g),ts))   => rigidrigid thy (env,binders,f,g,ss,ts)
       | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts)