# HG changeset patch
# User huffman
# Date 1242154885 25200
# Node ID 6dc708ca4a8fea085bfb41555894b52668efbbbe
# Parent  a27d4254ff4c4e65fa77e0b8ae9d95046b7f1864
add cpo_type function

diff -r a27d4254ff4c -r 6dc708ca4a8f 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;