equal
deleted
inserted
replaced
54 val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () |
54 val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () |
55 val ord = effective_term_order ctxt atp |
55 val ord = effective_term_order ctxt atp |
56 val _ = problem |
56 val _ = problem |
57 |> lines_of_atp_problem format ord (K []) |
57 |> lines_of_atp_problem format ord (K []) |
58 |> File.write_list prob_file |
58 |> File.write_list prob_file |
59 val exec = exec false |
|
60 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
59 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
61 val command = |
60 val command = |
62 File.bash_path (Path.explode path) ^ " " ^ |
61 File.bash_path (Path.explode path) ^ " " ^ |
63 arguments ctxt false "" atp_timeout (File.bash_path prob_file) |
62 arguments ctxt false "" atp_timeout (File.bash_path prob_file) |
64 (ord, K [], K []) |
63 (ord, K [], K []) |