--- a/src/HOL/HOLCF/Domain.thy Sat Jun 02 22:14:35 2018 +0200
+++ b/src/HOL/HOLCF/Domain.thy Sat Jun 02 22:39:45 2018 +0200
@@ -341,12 +341,12 @@
setup \<open>
fold Domain_Take_Proofs.add_rec_type
- [(@{type_name cfun}, [true, true]),
- (@{type_name "sfun"}, [true, true]),
- (@{type_name ssum}, [true, true]),
- (@{type_name sprod}, [true, true]),
- (@{type_name prod}, [true, true]),
- (@{type_name "u"}, [true])]
+ [(\<^type_name>\<open>cfun\<close>, [true, true]),
+ (\<^type_name>\<open>sfun\<close>, [true, true]),
+ (\<^type_name>\<open>ssum\<close>, [true, true]),
+ (\<^type_name>\<open>sprod\<close>, [true, true]),
+ (\<^type_name>\<open>prod\<close>, [true, true]),
+ (\<^type_name>\<open>u\<close>, [true])]
\<close>
end