# HG changeset patch
# User haftmann
# Date 1222327686 -7200
# Node ID 4f2406ddd9ea64e97884ab8111f566a895a4a953
# Parent  3cb64932ac77a6a403ef9f1a4b730c16d4283272
matchess

diff -r 3cb64932ac77 -r 4f2406ddd9ea src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Sep 25 09:28:05 2008 +0200
+++ b/src/Pure/pattern.ML	Thu Sep 25 09:28:06 2008 +0200
@@ -22,6 +22,7 @@
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val matches: theory -> term * term -> bool
+  val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val matches_subterm: theory -> term * term -> bool
   val unify: theory -> term * term -> Envir.env -> Envir.env
@@ -390,6 +391,8 @@
 
 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
 
+fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+
 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);