clarified File.platform_path vs. File.shell_path;
tuned;

--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Oct 15 15:45:50 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Oct 15 15:53:33 2009 +0200
@@ -59,8 +59,8 @@
     val output_file = filename dir "sos_out"
     val (output, rv) = system_out (
       if File.exists cmd then space_implode " "
-        [File.shell_path cmd, File.platform_path input_file, File.platform_path output_file]
-      else error ("Bad executable: " ^ File.shell_path cmd))
+        [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
+      else error ("Bad executable: " ^ File.platform_path cmd))
  
     (* read and analysize output *)
     val (res, res_msg) = find_failure rv

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 15:45:50 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 15 15:53:33 2009 +0200
@@ -53,7 +53,7 @@
 
 (** generic ATP wrapper **)
 
-(* hooks for writing problem files *)
+(* external problem files *)
 
 val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" "";
   (*Empty string means create files in Isabelle's temporary files directory.*)
@@ -108,7 +108,7 @@
   |> tap (after path);
 
 fun external_prover relevance_filter prepare write cmd args find_failure produce_answer
-  axiom_clauses filtered_clauses name subgoalno goal =
+    axiom_clauses filtered_clauses name subgoalno goal =
   let
     (* get clauses and prepare them for writing *)
     val (ctxt, (chain_ths, th)) = goal;
@@ -141,7 +141,7 @@
 
     (* write out problem file and call prover *)
     fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
-      [File.shell_path cmd, args, File.platform_path probfile] ^ " ; } 2>&1"
+      [File.shell_path cmd, args, File.shell_path probfile] ^ " ; } 2>&1"
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");