src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 53492 c3d7d9911aae
parent 53480 247817dbb990
child 53500 53b9326196fe
equal deleted inserted replaced
53491:2479b39d9d09 53492:c3d7d9911aae
   837                                        lam_trans uncurried_aliases
   837                                        lam_trans uncurried_aliases
   838                                        readable_names true hyp_ts concl_t
   838                                        readable_names true hyp_ts concl_t
   839             fun sel_weights () = atp_problem_selection_weights atp_problem
   839             fun sel_weights () = atp_problem_selection_weights atp_problem
   840             fun ord_info () = atp_problem_term_order_info atp_problem
   840             fun ord_info () = atp_problem_term_order_info atp_problem
   841             val ord = effective_term_order ctxt name
   841             val ord = effective_term_order ctxt name
   842             val full_proof =
   842             val full_proof = isar_proofs |> the_default (mode = Minimize)
   843               debug orelse (isar_proofs |> the_default (mode = Minimize))
       
   844             val args =
   843             val args =
   845               arguments ctxt full_proof extra
   844               arguments ctxt full_proof extra
   846                         (slice_timeout |> the_default one_day)
   845                         (slice_timeout |> the_default one_day)
   847                         (File.shell_path prob_path) (ord, ord_info, sel_weights)
   846                         (File.shell_path prob_path) (ord, ord_info, sel_weights)
   848             val command =
   847             val command =