--- a/src/HOL/HOLCF/Sprod.thy Wed Nov 30 16:27:10 2011 +0100
+++ b/src/HOL/HOLCF/Sprod.thy Wed Nov 30 17:30:01 2011 +0100
@@ -13,9 +13,10 @@
subsection {* Definition of strict product type *}
-pcpodef ('a, 'b) sprod (infixr "**" 20) =
- "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
-by simp_all
+definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
+
+pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
+ unfolding sprod_def by simp_all
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])