Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected problem with type abbreviations in pcpo_type
authoroheimb
Tue, 13 May 1997 15:02:19 +0200
changeset 3176 a3db6c177885
parent 3175 02d32516bc92
child 3177 3c1448b9b0ee
corrected problem with type abbreviations in pcpo_type
src/HOLCF/domain/library.ML file | annotate | diff | comparison | revisions 
--- 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 ----- *)
isabelle