--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Sat Jan 05 17:24:33 2019 +0100
@@ -408,7 +408,7 @@
nitpick [expect = genuine]
oops
-subsubsection \<open>@{const undefined}\<close>
+subsubsection \<open>\<^const>\<open>undefined\<close>\<close>
lemma "undefined"
nitpick [expect = genuine]
@@ -426,7 +426,7 @@
nitpick [expect = genuine]
oops
-subsubsection \<open>@{const The}\<close>
+subsubsection \<open>\<^const>\<open>The\<close>\<close>
lemma "The P"
nitpick [expect = genuine]
@@ -448,7 +448,7 @@
nitpick [expect = genuine]
oops
-subsubsection \<open>@{const Eps}\<close>
+subsubsection \<open>\<^const>\<open>Eps\<close>\<close>
lemma "Eps P"
nitpick [expect = genuine]
@@ -525,7 +525,7 @@
subsubsection \<open>Subtypes (typedef), typedecl\<close>
-text \<open>A completely unspecified non-empty subset of @{typ "'a"}:\<close>
+text \<open>A completely unspecified non-empty subset of \<^typ>\<open>'a\<close>:\<close>
definition "myTdef = insert (undefined::'a) (undefined::'a set)"