src/Pure/pattern.ML
changeset 28348 4f2406ddd9ea
parent 26939 1035c89b4c02
child 29269 5c25a2012975
     1.1 --- a/src/Pure/pattern.ML	Thu Sep 25 09:28:05 2008 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Sep 25 09:28:06 2008 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val first_order_match: theory -> term * term
     1.5      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     1.6    val matches: theory -> term * term -> bool
     1.7 +  val matchess: theory -> term list * term list -> bool
     1.8    val equiv: theory -> term * term -> bool
     1.9    val matches_subterm: theory -> term * term -> bool
    1.10    val unify: theory -> term * term -> Envir.env -> Envir.env
    1.11 @@ -390,6 +391,8 @@
    1.12  
    1.13  fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.14  
    1.15 +fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.16 +
    1.17  fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
    1.18  
    1.19