1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Aug 02 16:17:52 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 03 09:51:28 2012 +0200
     1.3 @@ -435,12 +435,6 @@
     1.4  fun overlord_file_location_for_prover prover =
     1.5    (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
     1.6  
     1.7 -fun with_path cleanup after f path =
     1.8 -  Exn.capture f path
     1.9 -  |> tap (fn _ => cleanup path)
    1.10 -  |> Exn.release
    1.11 -  |> tap (after path)
    1.12 -
    1.13  fun proof_banner mode name =
    1.14    case mode of
    1.15      Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
    1.16 @@ -653,7 +647,7 @@
    1.17      val problem_file_name =
    1.18        Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
    1.19                    suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
    1.20 -    val problem_path_name =
    1.21 +    val prob_path =
    1.22        if dest_dir = "" then
    1.23          File.tmp_path problem_file_name
    1.24        else if File.exists (Path.explode dest_dir) then
    1.25 @@ -687,7 +681,7 @@
    1.26          val as_time =
    1.27            raw_explode #> Scan.read Symbol.stopper time #> the_default 0
    1.28        in (output, as_time t |> Time.fromMilliseconds) end
    1.29 -    fun run_on prob_file =
    1.30 +    fun run () =
    1.31        let
    1.32          (* If slicing is disabled, we expand the last slice to fill the entire
    1.33             time available. *)
    1.34 @@ -776,13 +770,13 @@
    1.35                                   (ord, ord_info, sel_weights)
    1.36              val command =
    1.37                "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
    1.38 -              File.shell_path prob_file ^ ")"
    1.39 +              File.shell_path prob_path ^ ")"
    1.40                |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
    1.41              val _ =
    1.42                atp_problem
    1.43                |> lines_for_atp_problem format ord ord_info
    1.44                |> cons ("% " ^ command ^ "\n")
    1.45 -              |> File.write_list prob_file
    1.46 +              |> File.write_list prob_path
    1.47              val ((output, run_time), (atp_proof, outcome)) =
    1.48                TimeLimit.timeLimit generous_slice_timeout
    1.49                                    Isabelle_System.bash_output command
    1.50 @@ -836,17 +830,16 @@
    1.51           ("", Time.zeroTime, [], SOME InternalError))
    1.52          |> fold maybe_run_slice actual_slices
    1.53        end
    1.54 -
    1.55      (* If the problem file has not been exported, remove it; otherwise, export
    1.56         the proof file too. *)
    1.57 -    fun cleanup prob_file =
    1.58 -      if dest_dir = "" then try File.rm prob_file else NONE
    1.59 -    fun export prob_file (_, (output, _, _, _)) =
    1.60 +    fun clean_up () =
    1.61 +      if dest_dir = "" then (try File.rm prob_path; ()) else ()
    1.62 +    fun export (_, (output, _, _, _)) =
    1.63        if dest_dir = "" then ()
    1.64 -      else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
    1.65 +      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
    1.66      val ((_, (_, pool, fact_names, _, sym_tab)),
    1.67           (output, run_time, atp_proof, outcome)) =
    1.68 -      with_path cleanup export run_on problem_path_name
    1.69 +      with_cleanup clean_up run () |> tap export
    1.70      val important_message =
    1.71        if mode = Normal andalso
    1.72           random_range 0 (atp_important_message_keep_quotient - 1) = 0 then