# HG changeset patch
# User wenzelm
# Date 1149537262 -7200
# Node ID a8c02d8b8b40de7f5f5f57a4138cf236edf072b0
# Parent  06cb6743adf69d20d24b4488ca3f6a5a22b88f1d
added matches_seq (left-to-right matching, intermediate beta-normalization);

diff -r 06cb6743adf6 -r a8c02d8b8b40 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Jun 05 21:54:21 2006 +0200
+++ b/src/Pure/pattern.ML	Mon Jun 05 21:54:22 2006 +0200
@@ -23,7 +23,7 @@
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val matches: theory -> term * term -> bool
-  val matches_list: theory -> (term * term) list -> bool
+  val matches_seq: theory -> term list -> term list -> bool
   val matches_subterm: theory -> term * term -> bool
   val unify: theory -> term * term -> Envir.env -> Envir.env
   val first_order: term -> bool
@@ -404,11 +404,15 @@
   val envir' = apfst (typ_match thy (pT, oT)) envir;
 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
 
-(*Predicate: does the pattern match the object?*)
 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
 
-fun matches_list thy pos =
-  (fold (match thy) pos (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+fun matches_seq thy ps os =
+  let
+    fun mtch (pat :: pats) (obj :: objs) env =
+          mtch pats objs (match thy (pairself Envir.beta_norm (Envir.subst_vars env pat, obj)) env)
+      | mtch [] [] env = env
+      | mtch _ _ _ = raise MATCH;
+  in (mtch ps os (Vartab.empty, Vartab.empty); true) handle MATCH => false end;
 
 
 (* Does pat match a subterm of obj? *)