--- a/src/HOLCF/Tools/Domain/domain.ML Wed Nov 10 14:20:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain.ML Wed Nov 10 14:59:52 2010 -0800
@@ -185,7 +185,7 @@
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort "domain"};
+fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"};
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
| read_sort thy NONE = Sign.defaultS 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 *}