diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -682,7 +682,7 @@
 qed
 
 text \<open>
-@{term NF} characterizes exactly the terms that are in normal form.
+\<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form.
 \<close>
   
 lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"