src/HOL/Matrix_LP/Cplex_tools.ML

     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
      | Option.Option => raise (Load_cplexResult "Option")
 
 exception Execute of string;
 
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
+fun tmp_file s = File.standard_path (File.tmp_path (Path.basic s));
 fun wrap s = "\""^s^"\"";
 
 fun solve_glpk prog =
     let
     val name = string_of_int (Time.toMicroseconds (Time.now ()))