# HG changeset patch
# User wenzelm
# Date 1150730344 -7200
# Node ID 8257e52164a16e2e4ffef46fc7e2c4d0a502efe1
# Parent  138e0684cda272a256c55d46d9cb24832568f3dc
matchers: try pattern_matchers only *after* general matching (The
  pattern version is not a faithful approximation because it falls back
  on first-order matching!);

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 =