# HG changeset patch
# User wenzelm
# Date 1451230809 -3600
# Node ID 97c06cfd31e59f8a4204cea05bdd6fc588ecbca0
# Parent  3c8c390a8f0a4ed648062aa576ca3f159fad481d
more symbols;

diff -r 3c8c390a8f0a -r 97c06cfd31e5 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 27 16:20:02 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 27 16:40:09 2015 +0100
@@ -1652,8 +1652,8 @@
   [((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),