--- a/src/HOLCF/Cfun.thy Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Cfun.thy Mon Oct 10 05:46:17 2005 +0200
@@ -22,7 +22,7 @@
lemma adm_cont: "adm cont"
by (rule admI, rule cont_lub_fun)
-cpodef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
+cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
by (simp add: Ex_cont adm_cont)
syntax (xsymbols)
--- a/src/HOLCF/Sprod.thy Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Sprod.thy Mon Oct 10 05:46:17 2005 +0200
@@ -15,7 +15,7 @@
subsection {* Definition of strict product type *}
-pcpodef (Sprod) ('a, 'b) "**" (infixr 20) =
+pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
"{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
by simp
--- a/src/HOLCF/Ssum.thy Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Ssum.thy Mon Oct 10 05:46:17 2005 +0200
@@ -15,7 +15,7 @@
subsection {* Definition of strict sum type *}
-pcpodef (Ssum) ('a, 'b) "++" (infixr 10) =
+pcpodef (Ssum) ('a, 'b) "++" (infixr "++" 10) =
"{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
by simp