19 struct |
19 struct |
20 |
20 |
21 open Sledgehammer_Util |
21 open Sledgehammer_Util |
22 open Sledgehammer_Fact |
22 open Sledgehammer_Fact |
23 open Sledgehammer_Prover |
23 open Sledgehammer_Prover |
|
24 open Sledgehammer_Prover_Minimize |
24 open Sledgehammer_MaSh |
25 open Sledgehammer_MaSh |
25 open Sledgehammer_Commands |
26 open Sledgehammer_Commands |
26 |
27 |
27 fun run_prover override_params fact_override i n ctxt goal = |
28 fun run_prover override_params fact_override i n ctxt goal = |
28 let |
29 let |
|
30 val thy = Proof_Context.theory_of ctxt |
29 val mode = Normal |
31 val mode = Normal |
30 val params as {provers, max_facts, ...} = default_params ctxt override_params |
32 val params as {provers, max_facts, ...} = default_params thy override_params |
31 val name = hd provers |
33 val name = hd provers |
32 val prover = get_prover ctxt mode name |
34 val prover = get_prover ctxt mode name |
33 val default_max_facts = default_max_facts_of_prover ctxt name |
35 val default_max_facts = default_max_facts_of_prover ctxt name |
34 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt |
36 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt |
35 val ho_atp = exists (is_ho_atp ctxt) provers |
37 val ho_atp = exists (is_ho_atp ctxt) provers |