equal
deleted
inserted
replaced
836 val _ = |
836 val _ = |
837 if verbose then |
837 if verbose then |
838 Output.urgent_message "Generating proof text..." |
838 Output.urgent_message "Generating proof text..." |
839 else |
839 else |
840 () |
840 () |
|
841 val atp_proof = (fn () => termify_atp_proof ctxt pool lifted sym_tab atp_proof) |
841 val isar_params = |
842 val isar_params = |
842 (debug, verbose, preplay_timeout, isar_compress, isar_try0, |
843 (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, |
843 pool, fact_names, lifted, sym_tab, atp_proof, goal) |
844 goal) |
844 val one_line_params = |
845 val one_line_params = |
845 (preplay, proof_banner mode name, used_facts, |
846 (preplay, proof_banner mode name, used_facts, |
846 choose_minimize_command ctxt params minimize_command name |
847 choose_minimize_command ctxt params minimize_command name |
847 preplay, |
848 preplay, |
848 subgoal, subgoal_count) |
849 subgoal, subgoal_count) |