equal
deleted
inserted
replaced
79 isar_proof, isar_shrink_factor, ...}) |
79 isar_proof, isar_shrink_factor, ...}) |
80 i n state name_thms_pairs = |
80 i n state name_thms_pairs = |
81 let |
81 let |
82 val thy = Proof.theory_of state |
82 val thy = Proof.theory_of state |
83 val prover = case atps of |
83 val prover = case atps of |
84 [atp_name] => get_prover thy atp_name |
84 [atp_name] => get_prover_fun thy atp_name |
85 | _ => error "Expected a single ATP." |
85 | _ => error "Expected a single ATP." |
86 val msecs = Time.toMilliseconds minimize_timeout |
86 val msecs = Time.toMilliseconds minimize_timeout |
87 val _ = |
87 val _ = |
88 priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ |
88 priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ |
89 " with a time limit of " ^ string_of_int msecs ^ " ms.") |
89 " with a time limit of " ^ string_of_int msecs ^ " ms.") |