matchers: fall back on plain first_order_matchers, not pattern;
authorwenzelm
Thu Jul 06 11:26:46 2006 +0200 (2006-07-06)
changeset 200209e7d3d06c643
parent 20019 283dfd5bd36b
child 20021 815393c02db9
matchers: fall back on plain first_order_matchers, not pattern;
src/Pure/unify.ML
     1.1 --- a/src/Pure/unify.ML	Wed Jul 05 23:51:22 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Thu Jul 06 11:26:46 2006 +0200
     1.3 @@ -615,8 +615,8 @@
     1.4  
     1.5  
     1.6  (*Pattern matching*)
     1.7 -fun pattern_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
     1.8 -  let val (tyenv', tenv') = fold (Pattern.match thy) pairs (tyenv, tenv)
     1.9 +fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
    1.10 +  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
    1.11    in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
    1.12    handle Pattern.MATCH => Seq.empty;
    1.13  
    1.14 @@ -659,7 +659,7 @@
    1.15        in
    1.16          Seq.append
    1.17            (Seq.map_filter result (smash_unifiers thy pairs' empty))
    1.18 -          (pattern_matchers thy pairs empty)
    1.19 +          (first_order_matchers thy pairs empty)
    1.20        end;
    1.21  
    1.22  fun matches_list thy ps os =