Fix lambda/typing example given 'perm_type' changes.

Extract a usable half-way point from nominal_datatype branch.

This replaces the is_perm predicate with a type embodying that predicate.
It doesn't include the subsequent work on allowing multiple 'atom' types.

Get lambda/typing directory to build again.

Had to deal with termScript stealing the \rightarrow syntax (I made
that theft local to termScript); and with tight equality.

Refactor simple type theory development by moving theory of contexts
as association lists on strings to a separate theory.

Make a new directory containing some work on simple typing for the
lambda calculus.