| changeset 447 | d1f827fa0a18 |
| parent 398 | 41f279b477e2 |
| child 546 | 36e40454e03e |
--- 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;