--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -71,7 +71,7 @@
    ("compress", "smart"),
    ("try0", "true"),
    ("smt_proofs", "true"),
-   ("suggest_of", "smart"),
+   ("instantiate", "smart"),
    ("minimize", "true"),
    ("slices", string_of_int (12 * Multithreading.max_threads ())),
    ("preplay_timeout", "1"),
@@ -97,7 +97,7 @@
    ("dont_minimize", "minimize"),
    ("dont_try0", "try0"),
    ("no_smt_proofs", "smt_proofs"),
-   ("dont_suggest_of", "suggest_of")]
+   ("dont_instantiate", "instantiate")]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -267,7 +267,7 @@
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_bool "smt_proofs"
-    val suggest_of = lookup_option lookup_bool "suggest_of"
+    val instantiate = lookup_option lookup_bool "instantiate"
     val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
     val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices")
     val timeout = lookup_time "timeout"
@@ -283,7 +283,7 @@
      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,
-     suggest_of = suggest_of, minimize = minimize, slices = slices, timeout = timeout,
+     instantiate = instantiate, minimize = minimize, slices = slices, timeout = timeout,
      preplay_timeout = preplay_timeout, expect = expect, cache_dir = cache_dir}
   end