--- a/src/HOL/TPTP/MaSh_Eval.thy Sun Dec 09 14:05:21 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Mon Dec 10 10:29:52 2012 +0100
@@ -23,12 +23,20 @@
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"
*}
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions"
- "/tmp/mash_eval.out"
+ Isabelle_System.mkdir (Path.explode prob_dir)
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ evaluate_mash_suggestions @{context} params (SOME prob_dir)
+ "/tmp/mash_suggestions" "/tmp/mash_eval.out"
else
()
*}