src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

     do_slice timeout 1 NONE Time.zeroTime
   end
 
 fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, ...})
-    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
     val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss

                fun isar_params () =
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                   goal)
 
                val one_line_params =
-                 (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal,
-                  subgoal_count)
+                 (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
              end,
            if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")