462 NONE => I |
462 NONE => I |
463 | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) |
463 | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) |
464 fun failed failure = |
464 fun failed failure = |
465 ({outcome = SOME failure, used_facts = [], used_from = [], |
465 ({outcome = SOME failure, used_facts = [], used_from = [], |
466 run_time = Time.zeroTime, |
466 run_time = Time.zeroTime, |
467 preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed |
467 preplay = Lazy.value (Sledgehammer_Provers.plain_metis, |
468 Sledgehammer_Provers.plain_metis), |
468 Sledgehammer_Reconstructor.Play_Failed), |
469 message = K "", message_tail = ""}, ~1) |
469 message = K "", message_tail = ""}, ~1) |
470 val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} |
470 val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} |
471 : Sledgehammer_Provers.prover_result, |
471 : Sledgehammer_Provers.prover_result, |
472 time_isa) = time_limit (Mirabelle.cpu_time (fn () => |
472 time_isa) = time_limit (Mirabelle.cpu_time (fn () => |
473 let |
473 let |