--- a/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 18:27:55 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 18:32:11 2021 +0100
@@ -8,7 +8,7 @@
sig
val get_url: unit -> string
val list_systems: unit -> {url: string, systems: string list}
- val run_system: {system: string, problem: string, extra: string, timeout: Time.time} ->
+ val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} ->
{output: string, timing: Time.time}
end
@@ -24,7 +24,9 @@
in {url = url, systems = systems} end
fun run_system {system, problem, extra, timeout} =
- cat_strings0 [get_url (), system, problem, extra, string_of_int (Time.toMilliseconds timeout)]
+ cat_strings0
+ [get_url (), system, Isabelle_System.absolute_path problem,
+ extra, string_of_int (Time.toMilliseconds timeout)]
|> \<^scala>\<open>SystemOnTPTP.run_system\<close>
|> split_strings0 |> (fn [output, timing] =>
{output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})