diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Partial_Function.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -226,7 +226,7 @@
 done
 
 
-text \<open>Rules for @{term mono_body}:\<close>
+text \<open>Rules for \<^term>\<open>mono_body\<close>:\<close>
 
 lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
 by (rule monotoneI) (rule leq_refl)
@@ -446,12 +446,12 @@
   using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
   unfolding fun_lub_def flat_lub_def by(auto 9 2)
 
-declaration \<open>Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
-  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
+declaration \<open>Partial_Function.init "tailrec" \<^term>\<open>tailrec.fixp_fun\<close>
+  \<^term>\<open>tailrec.mono_body\<close> @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
   (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
 
-declaration \<open>Partial_Function.init "option" @{term option.fixp_fun}
-  @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
+declaration \<open>Partial_Function.init "option" \<^term>\<open>option.fixp_fun\<close>
+  \<^term>\<open>option.mono_body\<close> @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
   (SOME @{thm fixp_induct_option})\<close>
 
 hide_const (open) chain