# HG changeset patch
# User wenzelm
# Date 1152178006 -7200
# Node ID 9e7d3d06c643bd2eeb4b8f96e061f7debf827199
# Parent  283dfd5bd36b95e68b9432eda4c3750eb3118df2
matchers: fall back on plain first_order_matchers, not pattern;

diff -r 283dfd5bd36b -r 9e7d3d06c643 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Jul 05 23:51:22 2006 +0200
+++ b/src/Pure/unify.ML	Thu Jul 06 11:26:46 2006 +0200
@@ -615,8 +615,8 @@
 
 
 (*Pattern matching*)
-fun pattern_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
-  let val (tyenv', tenv') = fold (Pattern.match thy) pairs (tyenv, tenv)
+fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
+  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
   handle Pattern.MATCH => Seq.empty;
 
@@ -659,7 +659,7 @@
       in
         Seq.append
           (Seq.map_filter result (smash_unifiers thy pairs' empty))
-          (pattern_matchers thy pairs empty)
+          (first_order_matchers thy pairs empty)
       end;
 
 fun matches_list thy ps os =