src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

    ("verbose", "false"),
    ("overlord", "false"),
    ("explicit_apply", "false"),
    ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
-   ("convergence", "320"),
+   ("relevance_convergence", "320"),
    ("theory_relevant", "smart"),
-   ("follow_defs", "false"),
+   ("defs_relevant", "false"),
    ("isar_proof", "false"),
    ("shrink_factor", "1"),
    ("minimize_timeout", "5 s")]
 
 val alias_params =

    ("no_overlord", "overlord"),
    ("partial_types", "full_types"),
    ("implicit_apply", "explicit_apply"),
    ("ignore_no_atp", "respect_no_atp"),
    ("theory_irrelevant", "theory_relevant"),
-   ("dont_follow_defs", "follow_defs"),
+   ("defs_irrelevant", "defs_relevant"),
    ("no_isar_proof", "isar_proof")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "full_types", "explicit_apply",
    "isar_proof", "shrink_factor", "minimize_timeout"]

     val full_types = lookup_bool "full_types"
     val explicit_apply = lookup_bool "explicit_apply"
     val respect_no_atp = lookup_bool "respect_no_atp"
     val relevance_threshold =
       0.01 * Real.fromInt (lookup_int "relevance_threshold")
-    val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
+    val relevance_convergence =
+      0.01 * Real.fromInt (lookup_int "relevance_convergence")
     val theory_relevant = lookup_bool_option "theory_relevant"
-    val follow_defs = lookup_bool "follow_defs"
+    val defs_relevant = lookup_bool "defs_relevant"
     val isar_proof = lookup_bool "isar_proof"
     val shrink_factor = Int.max (1, lookup_int "shrink_factor")
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
      full_types = full_types, explicit_apply = explicit_apply,
      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
-     convergence = convergence, theory_relevant = theory_relevant,
-     follow_defs = follow_defs, isar_proof = isar_proof,
-     shrink_factor = shrink_factor, timeout = timeout,
+     relevance_convergence = relevance_convergence,
+     theory_relevant = theory_relevant, defs_relevant = defs_relevant,
+     isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
      minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)