clarified Pattern.matchess;

--- 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);