equal
deleted
inserted
replaced
297 SH_ERROR |
297 SH_ERROR |
298 |
298 |
299 fun run_sh prover hard_timeout timeout dir st = |
299 fun run_sh prover hard_timeout timeout dir st = |
300 let |
300 let |
301 val (ctxt, goal) = Proof.get_goal st |
301 val (ctxt, goal) = Proof.get_goal st |
302 val ctxt' = ctxt |> is_some dir ? Config.put AtpWrapper.destdir (the dir) |
302 val ctxt' = if is_none dir then ctxt |
|
303 else Config.put AtpWrapper.destdir (the dir) ctxt |
303 val atp = prover (AtpWrapper.atp_problem_of_goal |
304 val atp = prover (AtpWrapper.atp_problem_of_goal |
304 (AtpManager.get_full_types ()) 1 (ctxt', goal)) |
305 (AtpManager.get_full_types ()) 1 (ctxt', goal)) |
305 |
306 |
306 val time_limit = |
307 val time_limit = |
307 (case hard_timeout of |
308 (case hard_timeout of |