src/Pure/logic.ML
changeset 447 d1f827fa0a18
parent 398 41f279b477e2
child 546 36e40454e03e
equal deleted inserted replaced
446:3ee5c9314efe 447:d1f827fa0a18
   139 fun mk_type ty = Const ("TYPE", itselfT ty);
   139 fun mk_type ty = Const ("TYPE", itselfT ty);
   140 
   140 
   141 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   141 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   142   | dest_type t = raise TERM ("dest_type", [t]);
   142   | dest_type t = raise TERM ("dest_type", [t]);
   143 
   143 
   144 (* class constraints: (| ty : c_class |) *)
   144 (** class constraints **)
   145 
   145 
   146 fun mk_inclass (ty, c) =
   146 fun mk_inclass (ty, c) =
   147   Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
   147   Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
   148 
   148 
   149 fun dest_inclass (t as Const (c_class, _) $ ty) =
   149 fun dest_inclass (t as Const (c_class, _) $ ty) =