--- 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
()
*}