diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -333,7 +333,7 @@
                                     {path=[a], rows=rows}
      val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
           handle Match => mk_functional_err "error in pattern-match translation"
-     val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
+     val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
      val finals = map row_of_pat patts2
      val originals = map (row_of_pat o #2) rows
      val dummy = case (subtract (op =) finals originals)