diff -r 020becec359c -r 610794dff23c src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -173,7 +173,7 @@
         ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
       |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
         @{prop False}
-      |> #1 |> sort_wrt (heading_sort_key o fst)
+      |> #1 |> sort_by (heading_sort_key o fst)
     val prelude = fst (split_last problem)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =