src/HOL/Tools/ATP_Manager/atp_wrapper.ML

          args, File.shell_path probfile] ^ " ; } 2>&1"
        else
          space_implode " " ["exec", File.shell_path cmd, args,
          File.shell_path probfile, "2>&1"]) ^
       (if overlord then
-         " | sed 's/,/, /g' | sed 's/\\([=|]\\)/ \\1 /g' | sed 's/! =/ !=/g' \
-         \| sed 's/  / /g'"
+         " | sed 's/,/, /g' \
+         \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
+         \| sed 's/! =/ !=/g' \
+         \| sed 's/  / /g' | sed 's/| |/||/g' \
+         \| sed 's/ = = =/===/g' \
+         \| sed 's/= = /== /g'"
        else
          "")
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");

 val remote_known_failures =
   [(["Remote-script could not extract proof"],
     "Error: The remote ATP proof is ill-formed.")]
 
 fun remote_prover_config prover_prefix args
-        ({known_failures, max_new_clauses, prefers_theory_relevant, ...}
+        ({known_failures, max_new_clauses, prefers_theory_relevant,
+          supports_isar_proofs, ...}
          : prover_config) : prover_config =
   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    arguments = (fn timeout =>
      args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
      the_system prover_prefix),
    known_failures = remote_known_failures @ known_failures,
    max_new_clauses = max_new_clauses,
    prefers_theory_relevant = prefers_theory_relevant,
-   supports_isar_proofs = false}
+   supports_isar_proofs = supports_isar_proofs}
 
 val remote_vampire =
   tptp_prover "remote_vampire"
               (remote_prover_config "Vampire---9" "" vampire_config)