# HG changeset patch # User wenzelm # Date 1618260338 -7200 # Node ID 23d2adc5489e00b82daa4effa8dd6d4a70461baa # Parent 12b3f78dde61f61e2edbcd66c9ecd02f49f0c3a4 compile; diff -r 12b3f78dde61 -r 23d2adc5489e src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Apr 12 22:41:51 2021 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Apr 12 22:45:38 2021 +0200 @@ -58,8 +58,8 @@ |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = - File.bash_path (Path.explode path) ^ " " ^ - arguments ctxt false "" atp_timeout prob_file (ord, K [], K []) + space_implode " " (File.bash_path (Path.explode path) :: + arguments ctxt false "" atp_timeout prob_file (ord, K [], K [])) val outcome = Timeout.apply atp_timeout Isabelle_System.bash_output command |> fst