src/HOLCF/Tools/Domain/domain.ML
changeset 40501 2ed71459136e
parent 40497 d2e876d6da8c
child 40737 2037021f034f
--- 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;