# HG changeset patch
# User wenzelm
# Date 1265464255 -3600
# Node ID d6e492cea6e45e63e03b044488ce3b40c617bde4
# Parent  5408e5207131096d52c6bbacb4bc9d6923156bae
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;

diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -54,10 +54,12 @@
 
     (* call solver *)
     val output_file = filename dir "sos_out"
-    val (output, rv) = system_out (
-      if File.exists cmd then space_implode " "
-        [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
-      else error ("Bad executable: " ^ File.platform_path cmd))
+    val (output, rv) =
+      bash_output
+       (if File.exists cmd then
+          space_implode " "
+            [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
+        else error ("Bad executable: " ^ File.platform_path cmd))
 
     (* read and analyze output *)
     val (res, res_msg) = find_failure rv
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Matrix/cplex/Cplex_tools.ML
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -1145,7 +1145,7 @@
     val cplex_path = getenv "GLPK_PATH"
     val cplex = if cplex_path = "" then "glpsol" else cplex_path
     val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
-    val answer = #1 (system_out command)
+    val answer = #1 (bash_output command)
     in
     let
         val result = load_glpkResult resultname
@@ -1178,7 +1178,7 @@
     val cplex = if cplex_path = "" then "cplex" else cplex_path
     val _ = write_script scriptname lpname resultname
     val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
-    val answer = "return code "^(Int.toString (system command))
+    val answer = "return code "^(Int.toString (bash command))
     in
     let
         val result = load_cplexResult resultname
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Sat Feb 06 14:50:55 2010 +0100
@@ -40,7 +40,7 @@
       val pmu =
         if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
         else eindhoven_home ^ "/pmu";
-    in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
+    in #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
 in
   fn cgoal =>
     let
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -498,7 +498,7 @@
       else mucke_home ^ "/mucke";
     val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     val _ = File.write mucke_input_file s;
-    val (result, _) = system_out (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
+    val (result, _) = bash_output (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
   in
     if not (!trace_mc) then (File.rm mucke_input_file) else (); 
     result
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -156,7 +156,7 @@
       else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
     val _ = tracing msg
   in
-    system_out (space_implode " " ("perl -w" ::
+    bash_output (space_implode " " ("perl -w" ::
       File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
       map File.shell_quote (solver @ args) @
       map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -168,7 +168,7 @@
     fun run_on probfile =
       if File.exists cmd then
         write probfile clauses
-        |> pair (apfst split_time' (system_out (cmd_line probfile)))
+        |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd);
 
     (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
@@ -306,7 +306,7 @@
 
 fun get_systems () =
   let
-    val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+    val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
   in
     if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
     else split_lines answer
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -1004,7 +1004,7 @@
   read_next_problems (Substring.full (File.read path), [], []) |>> rev ||> rev
 
 (* The fudge term below is to account for Kodkodi's slow start-up time, which
-   is partly due to the JVM and partly due to the ML "system" function. *)
+   is partly due to the JVM and partly due to the ML "bash" function. *)
 val fudge_ms = 250
 
 (* bool -> Time.time option -> int -> int -> problem list -> outcome *)
@@ -1053,7 +1053,7 @@
           val outcome =
             let
               val code =
-                system ("cd " ^ temp_dir ^ ";\n" ^
+                bash ("cd " ^ temp_dir ^ ";\n" ^
                         "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
                         \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
                         \$JAVA_LIBRARY_PATH\" \
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -282,7 +282,7 @@
   (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
 
   fun make_external_solver cmd writefn readfn fm =
-    (writefn fm; system cmd; readfn ());
+    (writefn fm; bash cmd; readfn ());
 
 (* ------------------------------------------------------------------------- *)
 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -62,11 +62,11 @@
       val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
       val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
       val svc_output_file = File.tmp_path (Path.basic "SVM_out");
-      val _ = (File.write svc_input_file svc_input;
-               #1 (system_out (check_valid ^ " -dump-result " ^
-                        File.shell_path svc_output_file ^
-                        " " ^ File.shell_path svc_input_file ^
-                        ">/dev/null 2>&1")))
+      val _ = File.write svc_input_file svc_input;
+      val _ =
+        bash_output (check_valid ^ " -dump-result " ^
+          File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
+          ">/dev/null 2>&1")
       val svc_output =
         (case try File.read svc_output_file of
           SOME out => out
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/General/file.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -14,7 +14,6 @@
   val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val isabelle_tool: string -> string -> int
-  val system_command: string -> unit
   eqtype ident
   val rep_ident: ident -> string
   val ident: Path.T -> ident option
@@ -75,11 +74,11 @@
         then SOME path
         else NONE
       end handle OS.SysErr _ => NONE) of
-    SOME path => system (shell_quote path ^ " " ^ args)
+    SOME path => bash (shell_quote path ^ " " ^ args)
   | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
 
 fun system_command cmd =
-  if system cmd <> 0 then error ("System command failed: " ^ cmd)
+  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
   else ();
 
 
@@ -116,7 +115,7 @@
               SOME id => id
             | NONE =>
                 let val (id, rc) =  (*potentially slow*)
-                  system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
+                  bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
                 in
                   if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
                   else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/General/secure.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -15,8 +15,8 @@
   val toplevel_pp: string list -> string -> unit
   val open_unsynchronized: unit -> unit
   val commit: unit -> unit
-  val system_out: string -> string * int
-  val system: string -> int
+  val bash_output: string -> string * int
+  val bash: string -> int
 end;
 
 structure Secure: SECURE =
@@ -61,12 +61,12 @@
 
 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
 
-val orig_system_out = system_out;
+val orig_bash_output = bash_output;
 
-fun system_out s = (secure_shell (); orig_system_out s);
+fun bash_output s = (secure_shell (); orig_bash_output s);
 
-fun system s =
-  (case system_out s of
+fun bash s =
+  (case bash_output s of
     ("", rc) => rc
   | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
 
@@ -78,5 +78,5 @@
 fun use s = Secure.use_file ML_Parse.global_context true s
   handle ERROR msg => (writeln msg; error "ML error");
 val toplevel_pp = Secure.toplevel_pp;
-val system_out = Secure.system_out;
-val system = Secure.system;
+val bash_output = Secure.bash_output;
+val bash = Secure.bash;
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/IsaMakefile	Sat Feb 06 14:50:55 2010 +0100
@@ -21,19 +21,18 @@
 
 ## Pure
 
-BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML			\
+BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML	\
   ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML	\
-  ML-Systems/ml_name_space.ML				\
-  ML-Systems/ml_pretty.ML ML-Systems/mosml.ML				\
-  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
-  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML		\
-  ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML			\
-  ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML			\
-  ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML			\
-  ML-Systems/proper_int.ML ML-Systems/smlnj.ML				\
-  ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
-  ML-Systems/timing.ML ML-Systems/time_limit.ML				\
-  ML-Systems/universal.ML ML-Systems/unsynchronized.ML
+  ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML			\
+  ML-Systems/mosml.ML ML-Systems/multithreading.ML			\
+  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
+  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
+  ML-Systems/polyml-5.2.ML ML-Systems/polyml-5.2.1.ML			\
+  ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
+  ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
+  ML-Systems/thread_dummy.ML ML-Systems/timing.ML			\
+  ML-Systems/time_limit.ML ML-Systems/universal.ML			\
+  ML-Systems/unsynchronized.ML
 
 RAW: $(OUT)/RAW
 
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/bash.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/bash.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -0,0 +1,43 @@
+(*  Title:      Pure/ML-Systems/bash.ML
+    Author:     Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+local
+
+fun read_file name =
+  let val is = TextIO.openIn name
+  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
+
+fun write_file name txt =
+  let val os = TextIO.openOut name
+  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
+
+in
+
+fun bash_output script =
+  let
+    val script_name = OS.FileSys.tmpName ();
+    val _ = write_file script_name script;
+
+    val output_name = OS.FileSys.tmpName ();
+
+    val status =
+      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
+        script_name ^ " /dev/null " ^ output_name);
+    val rc =
+      (case Posix.Process.fromStatus status of
+        Posix.Process.W_EXITED => 0
+      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+    val output = read_file output_name handle IO.Io _ => "";
+    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+  in (output, rc) end;
+
+end;
+
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -229,7 +229,7 @@
 
 in
 
-fun system_out script =
+fun bash_output script =
   let
     val script_name = OS.FileSys.tmpName ();
     val _ = write_file script_name script;
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val system_out: string -> string * int
+  val bash_output: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -156,9 +156,9 @@
 end;
 
 
-(* system shell processes, with propagation of interrupts *)
+(* GNU bash processes, with propagation of interrupts *)
 
-fun system_out script = with_attributes no_interrupts (fn orig_atts =>
+fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
   let
     val script_name = OS.FileSys.tmpName ();
     val _ = write_file script_name script;
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -9,7 +9,7 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/timing.ML";
-use "ML-Systems/system_shell.ML";
+use "ML-Systems/bash.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
 
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -14,7 +14,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/timing.ML";
-use "ML-Systems/system_shell.ML";
+use "ML-Systems/bash.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
@@ -179,7 +179,7 @@
 
 (* system command execution *)
 
-val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
+val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
 
 fun process_id pid =
   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/system_shell.ML
--- a/src/Pure/ML-Systems/system_shell.ML	Sat Feb 06 14:39:33 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      Pure/ML-Systems/system_shell.ML
-    Author:     Makarius
-
-Generic system shell processes (no provisions to propagate interrupts;
-might still work via the controlling tty).
-*)
-
-local
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun system_out script =
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val output_name = OS.FileSys.tmpName ();
-
-    val status =
-      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
-        script_name ^ " /dev/null " ^ output_name);
-    val rc =
-      (case Posix.Process.fromStatus status of
-        Posix.Process.W_EXITED => 0
-      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
-      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
-      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-  in (output, rc) end;
-
-end;
-
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 06 14:50:55 2010 +0100
@@ -162,7 +162,7 @@
 
   /** system tools **/
 
-  def system_out(script: String): (String, Int) =
+  def bash_output(script: String): (String, Int) =
   {
     Standard_System.with_tmp_file("isabelle_script") { script_file =>
       Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/Thy/present.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -328,7 +328,7 @@
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));
     val _ = if verbose then writeln s else ();
-    val (out, rc) = system_out s;
+    val (out, rc) = bash_output s;
     val _ =
       if not (File.exists doc_path) orelse rc <> 0 then
         cat_error out ("Failed to build document " ^ quote (show_path doc_path))
diff -r 5408e5207131 -r d6e492cea6e4 src/Tools/Compute_Oracle/am_ghc.ML
--- a/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -228,7 +228,7 @@
         val module_file = tmp_file (module^".hs")
         val object_file = tmp_file (module^".o")
         val _ = writeTextFile module_file source
-        val _ = system ((!ghc)^" -c "^module_file)
+        val _ = bash ((!ghc)^" -c "^module_file)
         val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
     in
         (guid, module_file, arity)      
@@ -309,7 +309,7 @@
         val term = print_term arity_of 0 t
         val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
         val _ = writeTextFile call_file call_source
-        val _ = system ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
+        val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
         val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
         val t' = parse_result arity_of result
         val _ = OS.FileSys.remove call_file