diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/String.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -10,7 +10,7 @@
 
 text \<open>
   When modelling strings, we follow the approach given
-  in @{url "https://utf8everywhere.org/"}:
+  in \<^url>\<open>https://utf8everywhere.org/\<close>:
 
   \<^item> Strings are a list of bytes (8 bit).
 
@@ -668,9 +668,9 @@
 | constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) <= _)"
     and (OCaml) "!((_ : string) <= _)"
-    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
+    \<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only
           if no type class instance needs to be generated, because String = [Char] in Haskell
-          and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
+          and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close>
     and (Haskell) infix 4 "<="
     and (Scala) infixl 4 "<="
     and (Eval) infixl 6 "<="