Begin to make pretypes purely functional

I want to do without the references that are used in the unification
algorithm.