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