# HG changeset patch
# User wenzelm
# Date 1331405372 -3600
# Node ID 628b4a3fbf6eb76a1ed3630abb11cc12ec3cd3ce
# Parent  28909eecdf5b878302fcf8bbc5f4f24f5dd3bb1a
clarified Pattern.matchess;

diff -r 28909eecdf5b -r 628b4a3fbf6e src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sat Mar 10 17:07:10 2012 +0100
+++ b/src/Pure/pattern.ML	Sat Mar 10 19:49:32 2012 +0100
@@ -399,7 +399,9 @@
 
 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 matchess thy (ps, os) =
+  length ps = length os andalso
+    ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
 
 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);