src/HOL/Matrix/Cplex_tools.ML
changeset 43850 7f2cbc713344
parent 43602 8c89a1fb30f2
child 46531 eff798e48efc
     1.1 --- a/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ b/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:52:41 2011 +0200
     1.3 @@ -1141,7 +1141,7 @@
     1.4      val cplex_path = getenv "GLPK_PATH"
     1.5      val cplex = if cplex_path = "" then "glpsol" else cplex_path
     1.6      val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
     1.7 -    val answer = #1 (bash_output command)
     1.8 +    val answer = #1 (Isabelle_System.bash_output command)
     1.9      in
    1.10      let
    1.11          val result = load_glpkResult resultname
    1.12 @@ -1174,7 +1174,7 @@
    1.13      val cplex = if cplex_path = "" then "cplex" else cplex_path
    1.14      val _ = write_script scriptname lpname resultname
    1.15      val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
    1.16 -    val answer = "return code " ^ string_of_int (bash command)
    1.17 +    val answer = "return code " ^ string_of_int (Isabelle_System.bash command)
    1.18      in
    1.19      let
    1.20          val result = load_cplexResult resultname