--- a/src/HOL/TPTP/MaSh_Eval.thy Thu Dec 13 15:39:07 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Dec 13 22:49:06 2012 +0100
@@ -11,7 +11,7 @@
ML_file "mash_eval.ML"
sledgehammer_params
- [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+ [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
declare [[sledgehammer_instantiate_inducts]]
@@ -42,7 +42,7 @@
ML {*
if do_it then
evaluate_mash_suggestions @{context} params (SOME prob_dir)
- (prefix ^ "mash_suggestions") (prefix ^ "/tmp/mash_eval.out")
+ (prefix ^ "mash_suggestions") (prefix ^ "mash_eval")
else
()
*}