added logicC: class, logicS: sort;
added itselfT: typ -> typ, a_itselfT: typ (for axclasses);

--- a/src/Pure/term.ML	Wed May 18 15:19:25 1994 +0200
+++ b/src/Pure/term.ML	Wed May 18 15:20:54 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	term.ML
+(*  Title: 	Pure/term.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
@@ -213,6 +213,12 @@
 
 (** Connectives of higher order logic **)
 
+val logicC: class = "logic";
+val logicS: sort = [logicC];
+
+fun itselfT ty = Type ("itself", [ty]);
+val a_itselfT = itselfT (TFree ("'a", logicS));
+
 val propT : typ = Type("prop",[]);
 
 val implies = Const("==>", propT-->propT-->propT);