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