re-use Pattern.unify_types, including its trace_unify_fail option;

--- a/src/Pure/pattern.ML	Fri May 24 14:00:10 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 14:31:44 2013 +0200
@@ -24,6 +24,7 @@
   val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val matches_subterm: theory -> term * term -> bool
+  val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
   val unify: theory -> term * term -> Envir.env -> Envir.env
   val first_order: term -> bool
   val pattern: term -> bool

--- a/src/Pure/unify.ML	Fri May 24 14:00:10 2013 +0200
+++ b/src/Pure/unify.ML	Fri May 24 14:31:44 2013 +0200
@@ -207,14 +207,8 @@
 exception ASSIGN;  (*Raised if not an assignment*)
 
 
-fun unify_types thy (T, U) env =
-  if T = U then env
-  else
-    let
-      val Envir.Envir {maxidx, tenv, tyenv} = env;
-      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
-    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
-    handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy TU env =
+  Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
 
 fun test_unify_types thy (T, U) env =
   let