equal
deleted
inserted
replaced
676 I) |
676 I) |
677 |>> (if measure_run_time then split_time else rpair NONE) |
677 |>> (if measure_run_time then split_time else rpair NONE) |
678 val (atp_proof, outcome) = |
678 val (atp_proof, outcome) = |
679 extract_tstplike_proof_and_outcome verbose complete |
679 extract_tstplike_proof_and_outcome verbose complete |
680 proof_delims known_failures output |
680 proof_delims known_failures output |
681 |>> atp_proof_from_tstplike_proof atp_problem |
681 |>> atp_proof_from_tstplike_proof atp_problem output |
682 handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete) |
682 handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete) |
683 val (conjecture_shape, facts_offset, fact_names, |
|
684 typed_helpers) = |
|
685 if is_none outcome then |
|
686 repair_conjecture_shape_and_fact_names output |
|
687 conjecture_shape facts_offset fact_names typed_helpers |
|
688 else |
|
689 (* don't bother repairing *) |
|
690 (conjecture_shape, facts_offset, fact_names, typed_helpers) |
|
691 val outcome = |
683 val outcome = |
692 case outcome of |
684 case outcome of |
693 NONE => |
685 NONE => |
694 used_facts_in_unsound_atp_proof ctxt |
686 used_facts_in_unsound_atp_proof ctxt |
695 conjecture_shape facts_offset fact_names atp_proof |
687 conjecture_shape facts_offset fact_names atp_proof |