--- 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),