# HG changeset patch
# User wenzelm
# Date 1144622033 -7200
# Node ID 9f69613362c193145e65a9fa2f4bcbe1ce3e31d9
# Parent  78d6b7a01b12b04054cec0dba5ff488775c481b6
added aT (from axclass.ML);
non-pervasive itselfT, a_itselfT;

diff -r 78d6b7a01b12 -r 9f69613362c1 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Apr 10 00:33:52 2006 +0200
+++ b/src/Pure/term.ML	Mon Apr 10 00:33:53 2006 +0200
@@ -84,8 +84,6 @@
   structure Vartab: TABLE
   structure Typtab: TABLE
   structure Termtab: TABLE
-  val itselfT: typ -> typ
-  val a_itselfT: typ
   val propT: typ
   val implies: term
   val all: typ -> term
@@ -162,6 +160,9 @@
 signature TERM =
 sig
   include BASIC_TERM
+  val aT: sort -> typ
+  val itselfT: typ -> typ
+  val a_itselfT: typ
   val argument_type_of: term -> typ
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
@@ -695,6 +696,8 @@
 
 (** Connectives of higher order logic **)
 
+fun aT S = TFree ("'a", S);
+
 fun itselfT ty = Type ("itself", [ty]);
 val a_itselfT = itselfT (TFree ("'a", []));