recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;

--- a/src/Pure/type.ML	Sat Nov 08 12:15:40 2014 +0100
+++ b/src/Pure/type.ML	Sat Nov 08 15:01:05 2014 +0100
@@ -436,11 +436,10 @@
 
 fun typ_match tsig =
   let
-    fun match (V as TVar (v, S), T) subs =
+    fun match (TVar (v, S), T) subs =
           (case lookup subs (v, S) of
             NONE =>
-              if V = T then subs
-              else if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
+              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
           | SOME U => if U = T then subs else raise TYPE_MATCH)
       | match (Type (a, Ts), Type (b, Us)) subs =
@@ -457,9 +456,9 @@
   (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
 
 (*purely structural matching*)
-fun raw_match (V as TVar (v, S), T) subs =
+fun raw_match (TVar (v, S), T) subs =
       (case lookup subs (v, S) of
-        NONE => if V = T then subs else Vartab.update_new (v, (S, T)) subs
+        NONE => Vartab.update_new (v, (S, T)) subs
       | SOME U => if U = T then subs else raise TYPE_MATCH)
   | raw_match (Type (a, Ts), Type (b, Us)) subs =
       if a <> b then raise TYPE_MATCH