src/Pure/type.ML

   val devar: tyenv -> typ -> typ
   val typ_match: tsig -> typ * typ -> tyenv -> tyenv
   val typ_instance: tsig -> typ * typ -> bool
   val raw_match: typ * typ -> tyenv -> tyenv
   val raw_matches: typ list * typ list -> tyenv -> tyenv
+  val could_match: typ * typ -> bool
+  val could_matches: typ list * typ list -> bool
   val raw_instance: typ * typ -> bool
   exception TUNIFY
   val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
   val raw_unify: typ * typ -> tyenv -> tyenv
   val raw_unifys: typ list * typ list -> tyenv -> tyenv

   | raw_match _ _ = raise TYPE_MATCH
 and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs)
   | raw_matches ([], []) subs = subs
   | raw_matches _ _ = raise TYPE_MATCH;
 
+(*fast matching filter*)
+fun could_match (Type (a, Ts), Type (b, Us)) = a = b andalso could_matches (Ts, Us)
+  | could_match (TFree (a, _), TFree (b, _)) = a = b
+  | could_match (TVar _, _) = true
+  | could_match _ = false
+and could_matches (T :: Ts, U :: Us) = could_match (T, U) andalso could_matches (Ts, Us)
+  | could_matches ([], []) = true
+  | could_matches _ = false;
+
 fun raw_instance (T, U) =
-  (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+  if could_match (U, T) then
+    (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+  else false;
 
 
 (* unification *)
 
 exception TUNIFY;