# HG changeset patch
# User wenzelm
# Date 769267254 -7200
# Node ID d7ae7ac22d4816f69e0faba3c2faa7a49059f929
# Parent  caf9a9b7f6058abe6c89c4e220aee9e48e2a70a8
added logicC: class, logicS: sort;
added itselfT: typ -> typ, a_itselfT: typ (for axclasses);

diff -r caf9a9b7f605 -r d7ae7ac22d48 src/Pure/term.ML
--- 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);