diff -r 9653bea4aa83 -r bc43f86c9598 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Feb 14 09:36:35 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 15 10:56:23 2023 +0100
@@ -53,6 +53,8 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("spy", "false"),
+   ("abduce", "smart"),
+   ("check_consistent", "smart"),
    ("type_enc", "smart"),
    ("strict", "false"),
    ("lam_trans", "smart"),
@@ -84,6 +86,8 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("dont_spy", "spy"),
+   ("dont_abduce", "abduce"),
+   ("dont_check_consistent", "check_consistent"),
    ("non_strict", "strict"),
    ("no_uncurried_aliases", "uncurried_aliases"),
    ("dont_learn", "learn"),
@@ -228,6 +232,16 @@
     val overlord = lookup_bool "overlord"
     val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
+    val check_consistent =
+      if mode = Auto_Try then
+        SOME false
+      else
+        lookup_option lookup_bool "check_consistent"
+    val abduce =
+      if mode = Auto_Try then
+        SOME false
+      else
+        lookup_option lookup_bool "abduce"
     val type_enc =
       if mode = Auto_Try then
         NONE
@@ -261,13 +275,14 @@
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
-     type_enc = type_enc, strict = strict, lam_trans = lam_trans,
-     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
-     induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
-     max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-     max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0,
-     smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout,
-     preplay_timeout = preplay_timeout, expect = expect}
+     abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict,
+     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
+     fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
+     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
+     max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs,
+     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+     minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params