diff -r 138e0684cda2 -r 8257e52164a1 src/Pure/unify.ML
--- 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 =