src/HOL/Tools/ATP/atp_problem_generate.ML

 val completish_helper_table =
   helper_table @
   [((predicator_name, true),
     @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
    ((app_op_name, true),
-    [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast}),
-     (General, @{lemma "EX p. (p x <-> p y) --> x = y" by blast})]),
+    [(General, @{lemma "\<exists>x. \<not> f x = g x \<or> f = g" by blast}),
+     (General, @{lemma "\<exists>p. (p x \<longleftrightarrow> p y) \<longrightarrow> x = y" by blast})]),
    (("fconj", false), @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fdisj", false), @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fimplies", false),
     @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
     |> map (pair Non_Rec_Def)),