diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Nitpick_Examples/Refute_Nits.thy
--- 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)"