diff -r 919fb49ba201 -r ae4dc5ac983f src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -63,6 +63,7 @@
    ("fact_thresholds", "0.45 0.85"),
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
+   ("max_proofs", "4"),
    ("isar_proofs", "smart"),
    ("compress", "smart"),
    ("try0", "true"),
@@ -259,6 +260,7 @@
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
+    val max_proofs = lookup_int "max_proofs"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
@@ -274,9 +276,9 @@
      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,
-     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-     minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
-     expect = expect}
+     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