# 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