# HG changeset patch
# User nipkow
# Date 1314363281 -7200
# Node ID 9ec0dcd351a442f9135e55c0fc8369c1c1aa1631
# Parent  369e8c28a61add7775521b5f905acd49353fb3c8# Parent  5e580115dfcd1f2e83e38af2cce98d267b690392
merged

diff -r 5e580115dfcd -r 9ec0dcd351a4 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 11:22:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 14:54:41 2011 +0200
@@ -1253,7 +1253,8 @@
 
 val default_sym_tab_entries : (string * sym_info) list =
   (prefixed_predicator_name,
-   {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
+   {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
+       (* FIXME: needed? *) ::
   (make_fixed_const NONE @{const_name undefined},
    {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
   ([tptp_false, tptp_true]
diff -r 5e580115dfcd -r 9ec0dcd351a4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 26 11:22:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 26 14:54:41 2011 +0200
@@ -536,6 +536,11 @@
   #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.keep_partial_instances false
 
+fun suffix_for_mode Auto_Try = "_auto_try"
+  | suffix_for_mode Try = "_try"
+  | suffix_for_mode Normal = ""
+  | suffix_for_mode Minimize = "_min"
+
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
    Linux appears to be the only ATP that does not honor its time limit. *)
 val atp_timeout_slack = seconds 1.0
@@ -557,7 +562,7 @@
       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
     val problem_file_name =
       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
-                  "_" ^ string_of_int subgoal)
+                  suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
     val problem_path_name =
       if dest_dir = "" then
         File.tmp_path problem_file_name