src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

 
 fun run_atp mode name
     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
      slice, minimize, timeout, preplay_timeout, ...} : params)
-    minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 

                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
                      minimize, atp_proof, goal)
                   end
 
                 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 "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^