src/Pure/unify.ML
changeset 19920 8257e52164a1
parent 19876 11d447d5d68c
child 20020 9e7d3d06c643
     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 =