diff -r 3fd83a0cc4bd -r c4c746bbf836 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 18:43:59 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 18:53:13 2013 +0100 @@ -41,9 +41,10 @@ ML {* if do_it then - evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir) - (prefix ^ "mash_suggestions") (prefix ^ "mash_prover_suggestions") - (prefix ^ "mash_eval") + evaluate_mash_suggestions @{context} params (1, NONE) + [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN] + (SOME prob_dir) (prefix ^ "mash_suggestions") + (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval") else () *}