diff -r 08d7aff8c7e6 -r 631ea563c20a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
@@ -1646,8 +1646,9 @@
    (("COMBC", false), @{thms Meson.COMBC_def}),
    (("COMBS", false), @{thms Meson.COMBS_def}),
    ((predicator_name, false), [not_ffalse, ftrue]),
-   (* FIXME: Metis doesn't like existentials in helpers *)
+(* FIXME: Metis doesn't like existentials in helpers
    ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
+*)
    (("fFalse", false), [not_ffalse]),
    (("fFalse", true), @{thms True_or_False}),
    (("fTrue", false), [ftrue]),