--- a/src/HOL/TPTP/MaSh_Export_Base.thy Thu Jul 08 17:43:35 2021 +0200
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy Fri Jul 09 17:58:17 2021 +0200
@@ -15,7 +15,6 @@
lam_trans = lifting, timeout = 2, dont_preplay, minimize]
declare [[sledgehammer_fact_duplicates = true]]
-declare [[sledgehammer_instantiate_inducts = false]]
hide_fact (open) HOL.ext
--- 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
--- a/src/HOL/TPTP/mash_eval.ML Thu Jul 08 17:43:35 2021 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 09 17:58:17 2021 +0200
@@ -36,9 +36,11 @@
fun print s = File.append report_path (s ^ "\n")
- val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
+ val {provers, max_facts, slice, type_enc, lam_trans, timeout, induction_rules, ...} =
+ default_params thy []
val prover = hd provers
val max_suggs = generous_max_suggestions (the max_facts)
+ val inst_inducts = induction_rules = SOME Instantiate
val method_of_file_name =
perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
@@ -53,7 +55,7 @@
val liness' = Ctr_Sugar_Util.transpose (map pad liness0)
val css = clasimpset_rule_table_of ctxt
- val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
+ val facts = all_facts ctxt true Keyword.empty_keywords [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
@@ -122,7 +124,7 @@
suggs
|> find_suggested_facts ctxt facts
|> map (fact_of_raw_fact #> nickify)
- |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+ |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
|> map fact_of_raw_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
@@ -141,7 +143,6 @@
else
zeros
- val inst_inducts = Config.get ctxt instantiate_inducts
val options =
["prover = " ^ prover,
"max_facts = " ^ string_of_int (the max_facts),
--- 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