--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Jan 10 15:25:09 2018 +0100
@@ -330,11 +330,11 @@
nitpick [expect = genuine]
oops
-lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
+lemma "(x \<equiv> (\<equiv>)) \<Longrightarrow> False"
nitpick [expect = genuine]
oops
-lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
+lemma "(x \<equiv> (\<Longrightarrow>)) \<Longrightarrow> False"
nitpick [expect = genuine]
oops
@@ -384,11 +384,11 @@
nitpick [expect = genuine]
oops
-lemma "P (op \<in>)"
+lemma "P (\<in>)"
nitpick [expect = genuine]
oops
-lemma "P (op \<in> x)"
+lemma "P ((\<in>) x)"
nitpick [expect = genuine]
oops