diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Inductive.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -270,8 +270,8 @@
 
 subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
 
-text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
-  @{term lfp} and @{term gfp}\<close>
+text \<open>Weakens the condition \<^term>\<open>X \<subseteq> f X\<close> to one expressed using both
+  \<^term>\<open>lfp\<close> and \<^term>\<open>gfp\<close>\<close>
 lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
   by (iprover intro: subset_refl monoI Un_mono monoD)
 
@@ -312,7 +312,7 @@
 lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A"
   by (auto intro!: coinduct3)
 
-text \<open>Monotonicity of @{term gfp}!\<close>
+text \<open>Monotonicity of \<^term>\<open>gfp\<close>!\<close>
 lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
   by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
 
@@ -535,7 +535,7 @@
         val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
         val ft = Case_Translation.case_tr true ctxt [x, cs];
       in lambda x ft end
-  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
+  in [(\<^syntax_const>\<open>_lam_pats_syntax\<close>, fun_tr)] end
 \<close>
 
 end