src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

         Path.append (Path.explode dest_dir) problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir ^ ".")
     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
-val command = Path.explode ("/Users/blanchet/misc/E-weights/PROVER/" ^ snd exec) (*###*)
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n");
         val (output, t) = s |> split |> split_last |> apfst cat_lines;
         fun as_num f = f >> (fst o read_int);