src/HOL/Matrix/cplex/Cplex_tools.ML

     val resultname = tmp_file (name^".txt")
     val _ = save_cplexFile lpname prog
     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
         val _ = OS.FileSys.remove lpname
         val _ = OS.FileSys.remove resultname

     val _ = save_cplexFile lpname prog
     val cplex_path = getenv "CPLEX_PATH"
     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
         val _ = OS.FileSys.remove lpname
         val _ = OS.FileSys.remove resultname