matchers: try pattern_matchers only *after* general matching (The
pattern version is not a faithful approximation because it falls back
on first-order matching!);

--- a/src/Pure/unify.ML	Sat Jun 17 19:38:01 2006 +0200
+++ b/src/Pure/unify.ML	Mon Jun 19 17:19:04 2006 +0200
@@ -658,8 +658,8 @@
         val empty = Envir.empty maxidx';
       in
         Seq.append
+          (Seq.map_filter result (smash_unifiers thy pairs' empty))
           (pattern_matchers thy pairs empty)
-          (Seq.map_filter result (smash_unifiers thy pairs' empty))
       end;
 
 fun matches_list thy ps os =