- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.
datatype ('a,'v) instr = Const 'v
| Load 'a
| Apply ('v binop)