--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sat Jan 05 17:24:33 2019 +0100
@@ -592,7 +592,7 @@
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
-text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
+text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
lemma STAR_cos_Infinitesimal_approx:
fixes x :: "'a::{real_normed_field,banach} star"