export add_tvarsT, add_tvars, add_vars, add_frees (would actually
belong to term.ML, but is apt to cause some confusion with the
fold-right versions there);
types 'v binop = 'v => 'v => 'v
datatype ('a,'v) expr = Cex 'v
| Vex 'a
| Bex ('v binop) (('a,'v) expr) (('a,'v) expr)