213 extract_proof_and_outcome res_code proof_delims known_failures output |
213 extract_proof_and_outcome res_code proof_delims known_failures output |
214 val (message, relevant_thm_names) = |
214 val (message, relevant_thm_names) = |
215 case outcome of |
215 case outcome of |
216 NONE => |
216 NONE => |
217 proof_text isar_proof |
217 proof_text isar_proof |
218 (pool, debug, shrink_factor, ctxt, conjecture_shape) |
218 (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape) |
219 (minimize_command, proof, internal_thm_names, th, subgoal) |
219 (minimize_command, proof, internal_thm_names, th, subgoal) |
220 | SOME failure => (string_for_failure failure ^ "\n", []) |
220 | SOME failure => (string_for_failure failure ^ "\n", []) |
221 in |
221 in |
222 {outcome = outcome, message = message, pool = pool, |
222 {outcome = outcome, message = message, pool = pool, |
223 relevant_thm_names = relevant_thm_names, |
223 relevant_thm_names = relevant_thm_names, |
224 atp_run_time_in_msecs = atp_run_time_in_msecs, output = output, |
224 atp_run_time_in_msecs = atp_run_time_in_msecs, output = output, |