src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

   val get_prover : Proof.context -> mode -> string -> prover
 
   val binary_min_facts : int Config.T
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
     Proof.state -> thm -> ((string * stature) * thm list) list ->
-    ((string * stature) * thm list) list option * ((proof_method * play_outcome) -> string)
+    ((string * stature) * thm list) list option
+    * (((string * stature) list * (proof_method * play_outcome)) -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
 end;
 
 structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
 struct