diff -r ee9c8d36318e -r 2ed71459136e 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 *}