# HG changeset patch
# User wenzelm
# Date 1527971985 -7200
# Node ID 6bf71e7762265fa8521c6ccd36d4adf0b93413f0
# Parent  46d5a9f428e1b3d0d2fd1d7d6f7d573550dad60e
more symbols;

diff -r 46d5a9f428e1 -r 6bf71e776226 src/HOL/HOLCF/Domain.thy
--- 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