equal
deleted
inserted
replaced
715 facts |
715 facts |
716 |> map untranslated_fact |
716 |> map untranslated_fact |
717 |> not sound |
717 |> not sound |
718 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
718 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
719 |> take num_facts |
719 |> take num_facts |
720 |> polymorphism_of_type_enc type_enc <> Polymorphic |
720 |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic |
721 ? monomorphize_facts |
721 ? monomorphize_facts |
722 |> map (apsnd prop_of) |
722 |> map (apsnd prop_of) |
723 |> prepare_atp_problem ctxt format prem_role type_enc |
723 |> prepare_atp_problem ctxt format prem_role type_enc |
724 atp_mode lam_trans uncurried_aliases |
724 atp_mode lam_trans uncurried_aliases |
725 readable_names true hyp_ts concl_t |
725 readable_names true hyp_ts concl_t |
748 |> fst |> split_time |
748 |> fst |> split_time |
749 |> (fn accum as (output, _) => |
749 |> (fn accum as (output, _) => |
750 (accum, |
750 (accum, |
751 extract_tstplike_proof_and_outcome verbose complete |
751 extract_tstplike_proof_and_outcome verbose complete |
752 proof_delims known_failures output |
752 proof_delims known_failures output |
753 |>> atp_proof_from_tstplike_proof atp_problem output |
753 |>> atp_proof_from_tstplike_proof atp_problem |
754 handle UNRECOGNIZED_ATP_PROOF () => |
754 handle UNRECOGNIZED_ATP_PROOF () => |
755 ([], SOME ProofIncomplete))) |
755 ([], SOME ProofIncomplete))) |
756 handle TimeLimit.TimeOut => |
756 handle TimeLimit.TimeOut => |
757 (("", slice_timeout), ([], SOME TimedOut)) |
757 (("", slice_timeout), ([], SOME TimedOut)) |
758 val outcome = |
758 val outcome = |