# HG changeset patch # User desharna # Date 1625846297 -7200 # Node ID 57423714c29dc2a5a3d2267660c8c0d081fea9a3 # Parent bec00c7ef8dd6c599bc43d8207891c7e0063d310 fixed HOL-TPTP following f58108b7a60c diff -r bec00c7ef8dd -r 57423714c29d src/HOL/TPTP/MaSh_Export_Base.thy --- 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 diff -r bec00c7ef8dd -r 57423714c29d src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r bec00c7ef8dd -r 57423714c29d src/HOL/TPTP/mash_eval.ML --- 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), diff -r bec00c7ef8dd -r 57423714c29d src/HOL/TPTP/mash_export.ML --- 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