diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Nonstandard_Analysis/HLim.thy
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -108,7 +108,7 @@
   by (simp add: NSLIM_def)
 
 
-subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
+subsubsection \<open>Equivalence of \<^term>\<open>filterlim\<close> and \<^term>\<open>NSLIM\<close>\<close>
 
 lemma LIM_NSLIM:
   assumes f: "f \<midarrow>a\<rightarrow> L"