1.1 --- a/src/Pure/pattern.ML	Sat Mar 10 17:07:10 2012 +0100
     1.2 +++ b/src/Pure/pattern.ML	Sat Mar 10 19:49:32 2012 +0100
     1.3 @@ -399,7 +399,9 @@
     1.4  
     1.5  fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
     1.6  
     1.7 -fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
     1.8 +fun matchess thy (ps, os) =
     1.9 +  length ps = length os andalso
    1.10 +    ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
    1.11  
    1.12  fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
    1.13