139 val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
139 val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
140 best_max_new_mono_instances, ...} = get_atp thy name () |
140 best_max_new_mono_instances, ...} = get_atp thy name () |
141 |
141 |
142 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
142 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
143 val local_name = perhaps (try (unprefix remote_prefix)) name |
143 val local_name = perhaps (try (unprefix remote_prefix)) name |
144 val spassy = (local_name = pirateN orelse local_name = spassN) |
|
145 |
144 |
146 val completish = Config.get ctxt atp_completish |
145 val completish = Config.get ctxt atp_completish |
147 val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer |
146 val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer |
148 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
147 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
149 val (dest_dir, problem_prefix) = |
148 val (dest_dir, problem_prefix) = |
376 val metis_lam_trans = |
375 val metis_lam_trans = |
377 if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
376 if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
378 val atp_proof = |
377 val atp_proof = |
379 atp_proof |
378 atp_proof |
380 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |
379 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |
381 |> spassy ? introduce_spassy_skolems |
380 |> local_name = spassN ? introduce_spass_skolems |
382 |> factify_atp_proof (map fst used_from) hyp_ts concl_t |
381 |> factify_atp_proof (map fst used_from) hyp_ts concl_t |
383 in |
382 in |
384 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
383 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
385 minimize, atp_proof, goal) |
384 minimize, atp_proof, goal) |
386 end |
385 end |