minor performance tuning via fast matching filter;

--- a/src/Pure/defs.ML	Mon Mar 10 23:03:51 2014 +0100
+++ b/src/Pure/defs.ML	Tue Mar 11 10:14:45 2014 +0100
@@ -50,8 +50,10 @@
       handle Type.TUNIFY => true);
 
 fun match_args (Ts, Us) =
-  Option.map Envir.subst_type
-    (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
+  if Type.could_matches (Ts, Us) then
+    Option.map Envir.subst_type
+      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+  else NONE;
 
 
 (* datatype defs *)

--- a/src/Pure/type.ML	Mon Mar 10 23:03:51 2014 +0100
+++ b/src/Pure/type.ML	Tue Mar 11 10:14:45 2014 +0100
@@ -76,6 +76,8 @@
   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
@@ -461,8 +463,19 @@
   | 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 *)