--- a/src/HOL/TPTP/mash_export.ML Thu Jul 08 17:43:35 2021 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 09 17:58:17 2021 +0200
@@ -64,7 +64,7 @@
fun all_facts ctxt =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
- Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
+ Sledgehammer_Fact.all_facts ctxt true Keyword.empty_keywords [] [] css
|> sort (crude_thm_ord ctxt o apply2 snd)
end
@@ -172,7 +172,7 @@
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
null (the_list isar_deps) orelse
- is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
+ is_blacklisted_or_something (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
let