src/Pure/term.ML
changeset 4493 26511042ce07
parent 4487 9b4c1db5aca1
child 4604 ff8eca799c8f
equal deleted inserted replaced
4492:ab441d89a2cb 4493:26511042ce07
    32     Const of string * typ |
    32     Const of string * typ |
    33     Free of string * typ |
    33     Free of string * typ |
    34     Var of indexname * typ |
    34     Var of indexname * typ |
    35     Bound of int |
    35     Bound of int |
    36     Abs of string * typ * term |
    36     Abs of string * typ * term |
    37     op $ of term * term
    37     $ of term * term
    38   exception TYPE of string * typ list * term list
    38   exception TYPE of string * typ list * term list
    39   exception TERM of string * term list
    39   exception TERM of string * term list
    40   val is_Const: term -> bool
    40   val is_Const: term -> bool
    41   val is_Free: term -> bool
    41   val is_Free: term -> bool
    42   val is_Var: term -> bool
    42   val is_Var: term -> bool