tuned debugging file names
authorblanchet
Wed, 12 Dec 2012 13:42:14 +0100
changeset 50494 06b199a042ff
parent 50490 b977b727c7d5
child 50495 bd9a0028b063
tuned debugging file names
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 13:28:23 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 13:42:14 2012 +0100
@@ -624,11 +624,11 @@
          (max_new_instances |> the_default best_max_new_instances)
   #> Config.put Monomorph.keep_partial_instances false
 
-fun suffix_for_mode Auto_Try = "_auto_try"
+fun suffix_for_mode Auto_Try = "_try"
   | suffix_for_mode Try = "_try"
   | suffix_for_mode Normal = ""
-  | suffix_for_mode MaSh = "_mash"
-  | suffix_for_mode Auto_Minimize = "_auto_min"
+  | suffix_for_mode MaSh = ""
+  | suffix_for_mode Auto_Minimize = "_min"
   | suffix_for_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on