647 fun isar_proof_text ctxt isar_proofs |
647 fun isar_proof_text ctxt isar_proofs |
648 (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool, |
648 (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool, |
649 fact_names, lifted, sym_tab, atp_proof, goal) |
649 fact_names, lifted, sym_tab, atp_proof, goal) |
650 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
650 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
651 let |
651 let |
652 val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt |
652 val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
|
653 val (_, ctxt) = |
|
654 params |
|
655 |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) |
|
656 |> (fn fixes => |
|
657 ctxt |> Variable.set_body false |
|
658 |> Proof_Context.add_fixes fixes) |
653 val one_line_proof = one_line_proof_text 0 one_line_params |
659 val one_line_proof = one_line_proof_text 0 one_line_params |
654 val type_enc = |
660 val type_enc = |
655 if is_typed_helper_used_in_atp_proof atp_proof then full_typesN |
661 if is_typed_helper_used_in_atp_proof atp_proof then full_typesN |
656 else partial_typesN |
662 else partial_typesN |
657 val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans |
663 val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans |