matchers: try pattern_matchers only *after* general matching (The
authorwenzelm
Mon Jun 19 17:19:04 2006 +0200 (2006-06-19)
changeset 199208257e52164a1
parent 19919 138e0684cda2
child 19921 2a48a5550045
matchers: try pattern_matchers only *after* general matching (The
pattern version is not a faithful approximation because it falls back
on first-order matching!);
src/Pure/unify.ML
     1.1 --- a/src/Pure/unify.ML	Sat Jun 17 19:38:01 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Mon Jun 19 17:19:04 2006 +0200
     1.3 @@ -658,8 +658,8 @@
     1.4          val empty = Envir.empty maxidx';
     1.5        in
     1.6          Seq.append
     1.7 +          (Seq.map_filter result (smash_unifiers thy pairs' empty))
     1.8            (pattern_matchers thy pairs empty)
     1.9 -          (Seq.map_filter result (smash_unifiers thy pairs' empty))
    1.10        end;
    1.11  
    1.12  fun matches_list thy ps os =