diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sat Jul 16 20:14:58 2011 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sat Jul 16 20:52:41 2011 +0200 @@ -50,7 +50,7 @@ (* call solver *) val output_file = filename dir "sos_out" val (output, rv) = - bash_output + Isabelle_System.bash_output (if File.exists exe then space_implode " " (map File.shell_path [exe, input_file, output_file]) else error ("Bad executable: " ^ File.platform_path exe))