src/HOL/TPTP/atp_theory_export.ML
changeset 60641 f6e8293747fd
parent 59582 0fbed69ff081
child 60924 610794dff23c
--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 03 14:51:43 2015 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 03 16:19:45 2015 +0200
@@ -166,7 +166,7 @@
     val facts =
       Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
                                   Keyword.empty_keywords [] [] css_table
-      |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd)
+      |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
     val problem =
       facts
       |> map (fn ((_, loc), th) =>