equal
deleted
inserted
replaced
90 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." |
90 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." |
91 | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n |
91 | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n |
92 state axioms = |
92 state axioms = |
93 let |
93 let |
94 val thy = Proof.theory_of state |
94 val thy = Proof.theory_of state |
95 val prover = get_prover thy false prover_name |
95 val ctxt = Proof.context_of state |
|
96 val prover = get_prover ctxt false prover_name |
96 val msecs = Time.toMilliseconds timeout |
97 val msecs = Time.toMilliseconds timeout |
97 val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".") |
98 val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".") |
98 val {goal, ...} = Proof.goal state |
99 val {goal, ...} = Proof.goal state |
99 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
100 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
100 val explicit_apply = |
101 val explicit_apply = |