src/HOLCF/Tools/domain/domain_library.ML

--- a/src/HOLCF/Tools/domain/domain_library.ML	Tue May 12 11:37:40 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue May 12 12:01:25 2009 -0700
@@ -52,6 +52,7 @@
 signature DOMAIN_LIBRARY =
 sig
   val Imposs : string -> 'a;
+  val cpo_type : theory -> typ -> bool;
   val pcpo_type : theory -> typ -> bool;
   val string_of_typ : theory -> typ -> string;
 
@@ -190,6 +191,7 @@
       | index_vnames([],occupied) = [];
 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
 
+fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;