--- 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) ()