--- 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? *)