1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 26 10:12:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 26 10:25:13 2011 +0200
     1.3 @@ -536,6 +536,11 @@
     1.4    #> Config.put Monomorph.max_new_instances max_new_instances
     1.5    #> Config.put Monomorph.keep_partial_instances false
     1.6  
     1.7 +fun suffix_for_mode Auto_Try = "_auto_try"
     1.8 +  | suffix_for_mode Try = "_try"
     1.9 +  | suffix_for_mode Normal = ""
    1.10 +  | suffix_for_mode Minimize = "_min"
    1.11 +
    1.12  (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
    1.13     Linux appears to be the only ATP that does not honor its time limit. *)
    1.14  val atp_timeout_slack = seconds 1.0
    1.15 @@ -557,7 +562,7 @@
    1.16        else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
    1.17      val problem_file_name =
    1.18        Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
    1.19 -                  "_" ^ string_of_int subgoal)
    1.20 +                  suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
    1.21      val problem_path_name =
    1.22        if dest_dir = "" then
    1.23          File.tmp_path problem_file_name