equal
deleted
inserted
replaced
170 |
170 |
171 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state |
171 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state |
172 facts = |
172 facts = |
173 let |
173 let |
174 val ctxt = Proof.context_of state |
174 val ctxt = Proof.context_of state |
175 val prover = get_prover ctxt Minimize prover_name |
175 val prover = |
|
176 get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name |
176 val _ = print silent (fn () => "Sledgehammer minimizer: " ^ |
177 val _ = print silent (fn () => "Sledgehammer minimizer: " ^ |
177 quote prover_name ^ ".") |
178 quote prover_name ^ ".") |
178 fun test timeout = test_facts params silent prover timeout i n state |
179 fun test timeout = test_facts params silent prover timeout i n state |
179 in |
180 in |
180 (case test timeout facts of |
181 (case test timeout facts of |