equal
deleted
inserted
replaced
354 val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
354 val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
355 val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof |
355 val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof |
356 val preferred_methss = |
356 val preferred_methss = |
357 (Metis_Method (NONE, NONE), |
357 (Metis_Method (NONE, NONE), |
358 bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types |
358 bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types |
359 (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) |
359 (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) |
360 in |
360 in |
361 (used_facts, preferred_methss, |
361 (used_facts, preferred_methss, |
362 fn preplay => |
362 fn preplay => |
363 let |
363 let |
364 val _ = if verbose then writeln "Generating proof text..." else () |
364 val _ = if verbose then writeln "Generating proof text..." else () |