--- a/src/HOL/ex/SAT_Examples.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Thu Feb 15 12:11:00 2018 +0100
@@ -76,7 +76,7 @@
text \<open>eta-Equivalence\<close>
-lemma "(ALL x. P x) | ~ All P"
+lemma "(\<forall>x. P x) \<or> \<not> All P"
by sat
declare [[sat_trace = false]]