invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
clarified inlined command-line;
clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function);

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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Mar 14 18:32:11 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Mar 14 20:29:26 2021 +0100
@@ -46,6 +46,7 @@
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
   val is_vampire_noncommercial_license_accepted : unit -> bool option
+  val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
     string * (unit -> atp_config)
@@ -615,13 +616,15 @@
 
 val max_remote_secs = 1000   (* give Geoff Sutcliffe's servers a break *)
 
+val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"])
+
 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
-  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
+  {exec = isabelle_scala_function,
    arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ =>
-     (if command <> "" then "-c " ^ quote command ^ " " else "") ^
-     "-s " ^ the_remote_system system_name system_versions ^ " " ^
-     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
-     " " ^ File.bash_path problem,
+    (cat_strings0
+     [the_remote_system system_name system_versions,
+      Isabelle_System.absolute_path problem,
+      command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]),
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    prem_role = prem_role,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Mar 14 18:32:11 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Mar 14 20:29:26 2021 +0100
@@ -158,7 +158,7 @@
         Path.explode dest_dir + problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir)
-    val command0 =
+    val executable =
       (case find_first (fn var => getenv var <> "") (fst exec) of
         SOME var =>
         let
@@ -264,20 +264,27 @@
             val ord = effective_term_order ctxt name
             val args =
               arguments ctxt full_proofs extra slice_timeout prob_path (ord, ord_info, sel_weights)
-            val command = "exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args
+            val command = File.bash_path executable ^ " " ^ args
+
+            fun run_command () =
+              if exec = isabelle_scala_function then
+                let val {output, timing} = SystemOnTPTP.run_system_encoded args
+                in (output, timing) end
+              else
+                let val res = Isabelle_System.bash_process ("exec 2>&1; " ^ command)
+                in (Process_Result.out res, Process_Result.timing_elapsed res) end
 
             val _ =
               atp_problem
               |> lines_of_atp_problem format ord ord_info
-              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
+              |> (exec <> isabelle_scala_function) ?
+                cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
               |> File.write_list prob_path
 
             val ((output, run_time), (atp_proof, outcome)) =
-              Timeout.apply generous_slice_timeout Isabelle_System.bash_process command
-              |> (fn res =>
-                (Process_Result.out res |>
-                  (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I),
-                 Process_Result.timing_elapsed res))
+              Timeout.apply generous_slice_timeout run_command ()
+              |>> overlord ?
+                (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output)
               |> (fn accum as (output, _) =>
                 (accum,
                  extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
@@ -285,6 +292,7 @@
                    atp_problem
                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
               handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
+                | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg)))
 
             val outcome =
               (case outcome of