--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jul 08 17:23:01 2021 +0200
@@ -62,6 +62,7 @@
("uncurried_aliases", "smart"),
("learn", "true"),
("fact_filter", "smart"),
+ ("induction_rules", "smart"),
("max_facts", "smart"),
("fact_thresholds", "0.45 0.85"),
("max_mono_iters", "smart"),
@@ -260,7 +261,8 @@
val fact_filter =
lookup_option lookup_string "fact_filter"
|> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
- val induction_rules = lookup_option (the o induction_rules_of_string) "induction_rules"
+ val induction_rules =
+ lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules"
val max_facts = lookup_option lookup_int "max_facts"
val fact_thresholds = lookup_real_pair "fact_thresholds"
val max_mono_iters = lookup_option lookup_int "max_mono_iters"