src/Pure/term.ML
changeset 34922 e35f608f81a2
parent 33697 7d6793ce0a26
child 35227 d67857e3a8c0
equal deleted inserted replaced
34921:008126f730a0 34922:e35f608f81a2
    10 infixr --->;
    10 infixr --->;
    11 infix aconv;
    11 infix aconv;
    12 
    12 
    13 signature BASIC_TERM =
    13 signature BASIC_TERM =
    14 sig
    14 sig
    15   eqtype indexname
    15   type indexname = string * int
    16   eqtype class
    16   type class = string
    17   eqtype sort
    17   type sort = class list
    18   eqtype arity
    18   type arity = string * sort list * sort
    19   datatype typ =
    19   datatype typ =
    20     Type  of string * typ list |
    20     Type  of string * typ list |
    21     TFree of string * sort |
    21     TFree of string * sort |
    22     TVar  of indexname * sort
    22     TVar  of indexname * sort
    23   datatype term =
    23   datatype term =