src/HOLCF/Tutorial/Domain_ex.thy

--- a/src/HOLCF/Tutorial/Domain_ex.thy	Wed Nov 10 14:20:47 2010 -0800
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Wed Nov 10 14:59:52 2010 -0800
@@ -105,13 +105,13 @@
 
 text {* Lazy constructor arguments may have unpointed types. *}
 
-domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
+domain natlist = nnil | ncons (lazy "nat discr") natlist
 
 text {* Class constraints may be given for type parameters on the LHS. *}
 
-domain (unsafe) ('a::cpo) box = Box (lazy 'a)
+domain ('a::predomain) box = Box (lazy 'a)
 
-domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
+domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream"
 
 
 subsection {* Generated constants and theorems *}