fixed HOL-TPTP following f58108b7a60c
authordesharna
Fri, 09 Jul 2021 17:58:17 +0200
changeset 74204 57423714c29d
parent 74203 bec00c7ef8dd
child 74205 3aace56d282e
fixed HOL-TPTP following f58108b7a60c
src/HOL/TPTP/MaSh_Export_Base.thy
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
--- 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