# HG changeset patch
# User blanchet
# Date 1343292483 -7200
# Node ID c0f44941e674b3541b5dedf5e571659813306232
# Parent  7da5d3b8aef4e016bd3c18c9ff7f39c19fa383ba
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)

diff -r 7da5d3b8aef4 -r c0f44941e674 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -52,8 +52,8 @@
 local
 
 fun make_cmd command options problem_path proof_path = space_implode " " (
-  map File.shell_quote (command () @ options) @
-  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
+  "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
+  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
 
 fun trace_and ctxt msg f x =
   let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
diff -r 7da5d3b8aef4 -r c0f44941e674 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -775,9 +775,9 @@
             val args = arguments ctxt full_proof extra slice_timeout
                                  (ord, ord_info, sel_weights)
             val command =
-              File.shell_path command0 ^ " " ^ args ^ " " ^
-              File.shell_path prob_file
-              |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
+              File.shell_path prob_file ^ ")"
+              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
             val _ =
               atp_problem
               |> lines_for_atp_problem format ord ord_info