src/Provers/splitter.ML

               | _ => []
           in snd (fold iter ts (0, a)) end
   in posns Ts [] [] t end;
 
 fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
-  prod_ord (int_ord o pairself length) (order o pairself length)
+  prod_ord (int_ord o apply2 length) (order o apply2 length)
     ((ps, pos), (qs, qos));
 
 
 (************************************************************
    call split_posns with appropriate parameters