src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

 signature SLEDGEHAMMER_MINIMIZE =
 sig
   type locality = Sledgehammer_Filter.locality
   type params = Sledgehammer_Provers.params
 
-  val binary_threshold : int Unsynchronized.ref
+  val binary_min_facts : int Unsynchronized.ref
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
     string -> params -> bool -> int -> int -> Proof.state
     -> ((string * locality) * thm list) list
     -> ((string * locality) * thm list) list option * string

 (* The sublinear algorithm works well in almost all situations, except when the
    external prover cannot return the list of used facts and hence returns all
    facts as used. In that case, the binary algorithm is much more appropriate.
    We can usually detect the situation by looking at the number of used facts
    reported by the prover. *)
-val binary_threshold = Unsynchronized.ref 20
+val binary_min_facts = Unsynchronized.ref 20
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
 fun sublinear_minimize _ [] p = p
   | sublinear_minimize test (x :: xs) (seen, result) =

          val new_timeout =
            Int.min (msecs, Time.toMilliseconds time + slack_msecs)
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =
-           if length facts >= !binary_threshold then
+           if length facts >= !binary_min_facts then
              binary_minimize (do_test new_timeout) facts
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)
          val n = length min_thms
          val _ = print silent (fn () => cat_lines