compile;
authorwenzelm
Mon, 12 Apr 2021 22:45:38 +0200
changeset 73831 23d2adc5489e
parent 73830 12b3f78dde61
child 73832 b50f8cc8c08e
compile;
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