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