src/HOL/Tools/atp_wrapper.ML

     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
     val probfile = prob_pathname subgoalno
     val fname = File.platform_path probfile
     val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
     val cmdline =
-      if File.exists cmd then File.shell_path cmd ^ " " ^ args
+      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ fname)
 
     (* remove *temporary* files *)
     val _ = if destdir' = "" then OS.FileSys.remove fname else ()