src/Pure/unify.ML
changeset 19920 8257e52164a1
parent 19876 11d447d5d68c
child 20020 9e7d3d06c643
equal deleted inserted replaced
19919:138e0684cda2 19920:8257e52164a1
   656           else NONE;
   656           else NONE;
   657 
   657 
   658         val empty = Envir.empty maxidx';
   658         val empty = Envir.empty maxidx';
   659       in
   659       in
   660         Seq.append
   660         Seq.append
       
   661           (Seq.map_filter result (smash_unifiers thy pairs' empty))
   661           (pattern_matchers thy pairs empty)
   662           (pattern_matchers thy pairs empty)
   662           (Seq.map_filter result (smash_unifiers thy pairs' empty))
       
   663       end;
   663       end;
   664 
   664 
   665 fun matches_list thy ps os =
   665 fun matches_list thy ps os =
   666   length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
   666   length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
   667 
   667