--- a/src/HOL/TPTP/atp_theory_export.ML Thu Jul 08 17:43:35 2021 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 09 17:58:17 2021 +0200
@@ -160,8 +160,8 @@
val mono = not (is_type_enc_polymorphic type_enc)
val facts =
- Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
- Keyword.empty_keywords [] [] css_table
+ Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] []
+ css_table
|> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
val problem =
facts