src/HOL/HOLCF/Library/List_Predomain.thy

--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -61,7 +61,7 @@
 done
 
 text \<open>
-  Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
+  Types \<^typ>\<open>'a list u\<close>. and \<^typ>\<open>'a u slist\<close> are isomorphic.
 \<close>
 
 fixrec encode_list_u where
@@ -168,7 +168,7 @@
 done
 
 setup \<open>
-  Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
+  Domain_Take_Proofs.add_rec_type (\<^type_name>\<open>list\<close>, [true])
 \<close>
 
 end