author | wenzelm |
Wed, 06 Jul 1994 11:36:00 +0200 | |
changeset 447 | d1f827fa0a18 |
parent 446 | 3ee5c9314efe |
child 448 | d7ff85d292c7 |
src/Pure/logic.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/logic.ML Fri Jul 01 11:10:31 1994 +0200 +++ b/src/Pure/logic.ML Wed Jul 06 11:36:00 1994 +0200 @@ -141,7 +141,7 @@ fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty | dest_type t = raise TERM ("dest_type", [t]); -(* class constraints: (| ty : c_class |) *) +(** class constraints **) fun mk_inclass (ty, c) = Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;