added aT (from axclass.ML);
authorwenzelm
Mon Apr 10 00:33:53 2006 +0200 (2006-04-10)
changeset 193949f69613362c1
parent 19393 78d6b7a01b12
child 19395 edf92521e8d3
added aT (from axclass.ML);
non-pervasive itselfT, a_itselfT;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Mon Apr 10 00:33:52 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Mon Apr 10 00:33:53 2006 +0200
     1.3 @@ -84,8 +84,6 @@
     1.4    structure Vartab: TABLE
     1.5    structure Typtab: TABLE
     1.6    structure Termtab: TABLE
     1.7 -  val itselfT: typ -> typ
     1.8 -  val a_itselfT: typ
     1.9    val propT: typ
    1.10    val implies: term
    1.11    val all: typ -> term
    1.12 @@ -162,6 +160,9 @@
    1.13  signature TERM =
    1.14  sig
    1.15    include BASIC_TERM
    1.16 +  val aT: sort -> typ
    1.17 +  val itselfT: typ -> typ
    1.18 +  val a_itselfT: typ
    1.19    val argument_type_of: term -> typ
    1.20    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.21    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.22 @@ -695,6 +696,8 @@
    1.23  
    1.24  (** Connectives of higher order logic **)
    1.25  
    1.26 +fun aT S = TFree ("'a", S);
    1.27 +
    1.28  fun itselfT ty = Type ("itself", [ty]);
    1.29  val a_itselfT = itselfT (TFree ("'a", []));
    1.30