1.1 --- a/src/Pure/logic.ML	Thu May 26 13:45:43 1994 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu May 26 16:40:45 1994 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	logic
     1.5 +(*  Title: 	Pure/logic.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   Cambridge University 1992
     1.9 @@ -17,6 +17,8 @@
    1.10    val dest_equals: term -> term * term
    1.11    val dest_flexpair: term -> term * term
    1.12    val dest_implies: term -> term * term
    1.13 +  val dest_inclass: term -> typ * class
    1.14 +  val dest_type: term -> typ
    1.15    val flatten_params: int -> term -> term
    1.16    val freeze_vars: term -> term
    1.17    val incr_indexes: typ list * int -> term -> term
    1.18 @@ -27,6 +29,8 @@
    1.19    val mk_equals: term * term -> term
    1.20    val mk_flexpair: term * term -> term
    1.21    val mk_implies: term * term -> term
    1.22 +  val mk_inclass: typ * class -> term
    1.23 +  val mk_type: typ -> term
    1.24    val occs: term * term -> bool
    1.25    val rule_of: (term*term)list * term list * term -> term
    1.26    val set_rename_prefix: string -> unit   
    1.27 @@ -43,9 +47,11 @@
    1.28    val varify: term -> term  
    1.29    end;
    1.30  
    1.31 -functor LogicFun (structure Unify: UNIFY and Net:NET)(* : LOGIC *) =  (* FIXME *)
    1.32 +functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
    1.33  struct
    1.34 -structure Type = Unify.Sign.Type;
    1.35 +
    1.36 +structure Sign = Unify.Sign;
    1.37 +structure Type = Sign.Type;
    1.38  
    1.39  (*** Abstract syntax operations on the meta-connectives ***)
    1.40  
    1.41 @@ -128,6 +134,23 @@
    1.42    let val (tpairs,horn) = strip_flexpairs A 
    1.43    in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
    1.44  
    1.45 +(** types as terms **)
    1.46 +
    1.47 +fun mk_type ty = Const ("TYPE", itselfT ty);
    1.48 +
    1.49 +fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
    1.50 +  | dest_type t = raise TERM ("dest_type", [t]);
    1.51 +
    1.52 +(* class constraints: (| ty : c_class |) *)
    1.53 +
    1.54 +fun mk_inclass (ty, c) =
    1.55 +  Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
    1.56 +
    1.57 +fun dest_inclass (t as Const (c_class, _) $ ty) =
    1.58 +      ((dest_type ty, Sign.class_of_const c_class)
    1.59 +        handle TERM _ => raise TERM ("dest_inclass", [t]))
    1.60 +  | dest_inclass t = raise TERM ("dest_inclass", [t]);
    1.61 +
    1.62  
    1.63  (*** Low-level term operations ***)
    1.64