# HG changeset patch
# User huffman
# Date 1289429992 28800
# Node ID 2ed71459136e85f1540d70d463a636c048b2d6e5
# Parent  ee9c8d36318ee1f737c18e99ec3cb88aa63c0f76
allow unpointed lazy arguments for definitional domain package

diff -r ee9c8d36318e -r 2ed71459136e src/HOLCF/Tools/Domain/domain.ML
--- 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;
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 *}