equal
deleted
inserted
replaced
378 val metis_lam_trans = |
378 val metis_lam_trans = |
379 if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
379 if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
380 val atp_proof = |
380 val atp_proof = |
381 atp_proof |
381 atp_proof |
382 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |
382 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |
383 |> spass ? introduce_spass_skolem |
383 |> spass ? introduce_spass_skolems |
384 |> factify_atp_proof (map fst used_from) hyp_ts concl_t |
384 |> factify_atp_proof (map fst used_from) hyp_ts concl_t |
385 in |
385 in |
386 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
386 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
387 minimize, atp_proof, goal) |
387 minimize, atp_proof, goal) |
388 end |
388 end |