# HG changeset patch
# User blanchet
# Date 1355345943 -3600
# Node ID cacf3cdb32762e5206528a8ad00d83743a8c3451
# Parent  c283bc0a8f1aaee0aa20a309347d78bd8cf4d829
tuning

diff -r c283bc0a8f1a -r cacf3cdb3276 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 12 21:48:29 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 12 21:59:03 2012 +0100
@@ -27,7 +27,9 @@
 ML {*
 val do_it = false (* switch to "true" to generate the files *)
 val params = Sledgehammer_Isar.default_params @{context} []
-val prob_dir = "/tmp/mash_problems"
+val dir = "List"
+val prefix = "/tmp/" ^ dir ^ "/"
+val prob_dir = prefix ^ "mash_problems"
 *}
 
 ML {*
@@ -40,7 +42,7 @@
 ML {*
 if do_it then
   evaluate_mash_suggestions @{context} params (SOME prob_dir)
-      "/tmp/mash_suggestions" "/tmp/mash_eval.out"
+      (prefix ^ "mash_suggestions") (prefix ^ "/tmp/mash_eval.out")
 else
   ()
 *}
diff -r c283bc0a8f1a -r cacf3cdb3276 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 12 21:48:29 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 12 21:59:03 2012 +0100
@@ -25,7 +25,7 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
-val dir = space_implode "__" (map Context.theory_name thys)
+val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 *}