matchers: fall back on plain first_order_matchers, not pattern;

--- 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 =