src/Pure/term.ML

   val aconv: term * term -> bool
   val aconvs: term list * term list -> bool
   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
   val equals: typ -> term
   val strip_all_body: term -> term

 end;
 
 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
   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list

 end;
 
 
 (** Connectives of higher order logic **)
 
+fun aT S = TFree ("'a", S);
+
 fun itselfT ty = Type ("itself", [ty]);
 val a_itselfT = itselfT (TFree ("'a", []));
 
 val propT : typ = Type("prop",[]);