--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Dec 17 09:57:22 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sat Dec 18 13:27:42 2021 +0100
@@ -19,6 +19,7 @@
datatype induction_rules = Include | Exclude | Instantiate
val induction_rules_of_string : string -> induction_rules option
+ val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list
type params =
{debug : bool,
@@ -147,6 +148,10 @@
fun string_of_params (params : params) =
YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
+fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
+ induction_rules = Exclude ?
+ filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
+
fun set_params_provers params provers =
{debug = #debug params,
verbose = #verbose params,