# HG changeset patch
# User wenzelm
# Date 769963245 -7200
# Node ID 41f279b477e2110a8e1116c1b97d069c961c8ce9
# Parent  48cb3fa4bc596dc152359635ac96e9086aa1d9fb
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
restored functor sig constraint :LOGIC;

diff -r 48cb3fa4bc59 -r 41f279b477e2 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu May 26 13:45:43 1994 +0200
+++ b/src/Pure/logic.ML	Thu May 26 16:40:45 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	logic
+(*  Title: 	Pure/logic.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
@@ -17,6 +17,8 @@
   val dest_equals: term -> term * term
   val dest_flexpair: term -> term * term
   val dest_implies: term -> term * term
+  val dest_inclass: term -> typ * class
+  val dest_type: term -> typ
   val flatten_params: int -> term -> term
   val freeze_vars: term -> term
   val incr_indexes: typ list * int -> term -> term
@@ -27,6 +29,8 @@
   val mk_equals: term * term -> term
   val mk_flexpair: term * term -> term
   val mk_implies: term * term -> term
+  val mk_inclass: typ * class -> term
+  val mk_type: typ -> term
   val occs: term * term -> bool
   val rule_of: (term*term)list * term list * term -> term
   val set_rename_prefix: string -> unit   
@@ -43,9 +47,11 @@
   val varify: term -> term  
   end;
 
-functor LogicFun (structure Unify: UNIFY and Net:NET)(* : LOGIC *) =  (* FIXME *)
+functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
 struct
-structure Type = Unify.Sign.Type;
+
+structure Sign = Unify.Sign;
+structure Type = Sign.Type;
 
 (*** Abstract syntax operations on the meta-connectives ***)
 
@@ -128,6 +134,23 @@
   let val (tpairs,horn) = strip_flexpairs A 
   in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
 
+(** types as terms **)
+
+fun mk_type ty = Const ("TYPE", itselfT ty);
+
+fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
+  | dest_type t = raise TERM ("dest_type", [t]);
+
+(* class constraints: (| ty : c_class |) *)
+
+fun mk_inclass (ty, c) =
+  Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
+
+fun dest_inclass (t as Const (c_class, _) $ ty) =
+      ((dest_type ty, Sign.class_of_const c_class)
+        handle TERM _ => raise TERM ("dest_inclass", [t]))
+  | dest_inclass t = raise TERM ("dest_inclass", [t]);
+
 
 (*** Low-level term operations ***)