# HG changeset patch
# User oheimb
# Date 863528539 -7200
# Node ID a3db6c177885489ca823e7d56346b6e6104deced
# Parent  02d32516bc92453ade9465ea80e30d06063cdc24
corrected problem with type abbreviations in pcpo_type

diff -r 02d32516bc92 -r a3db6c177885 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Tue May 13 13:02:34 1997 +0200
+++ b/src/HOLCF/domain/library.ML	Tue May 13 15:02:19 1997 +0200
@@ -79,8 +79,10 @@
 fun rep_Type  (Type  x) = x | rep_Type  _ = Imposs "library:rep_Type";
 fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
 val tsig_of = #tsig o Sign.rep_sg o sign_of;
-fun pcpo_type thy t = Type.typ_instance(tsig_of thy,t,TVar(("'a",0),["pcpo"]));
-fun string_of_typ thy = Sign.string_of_typ (sign_of thy);
+fun pcpo_type thy t = Type.of_sort (tsig_of thy) 
+			(Sign.certify_typ (sign_of thy) t,["pcpo"]);
+fun string_of_typ thy t = let val sg = sign_of thy in
+			  Sign.string_of_typ sg (Sign.certify_typ sg t) end;
 
 (* ----- constructor list handling ----- *)