diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -26,9 +26,7 @@
 
 val max_facts_slack = 2
 
-val all_names =
-  filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params thy file_name =
   let