equal
deleted
inserted
replaced
608 |>> (if measure_run_time then split_time else rpair NONE) |
608 |>> (if measure_run_time then split_time else rpair NONE) |
609 val (atp_proof, outcome) = |
609 val (atp_proof, outcome) = |
610 extract_tstplike_proof_and_outcome verbose complete res_code |
610 extract_tstplike_proof_and_outcome verbose complete res_code |
611 proof_delims known_failures output |
611 proof_delims known_failures output |
612 |>> atp_proof_from_tstplike_proof atp_problem |
612 |>> atp_proof_from_tstplike_proof atp_problem |
|
613 handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete) |
613 val (conjecture_shape, facts_offset, fact_names, |
614 val (conjecture_shape, facts_offset, fact_names, |
614 typed_helpers) = |
615 typed_helpers) = |
615 if is_none outcome then |
616 if is_none outcome then |
616 repair_conjecture_shape_and_fact_names type_sys output |
617 repair_conjecture_shape_and_fact_names type_sys output |
617 conjecture_shape facts_offset fact_names typed_helpers |
618 conjecture_shape facts_offset fact_names typed_helpers |