improved the finite-support proof added finite support proof for options (I am surprised that one does not need more fs-proofs; at the moment only lists, products, units and atoms are shown to be finitely supported (of course also every nominal datatype is finitely supported)) deleted pt_bool_inst - not necessary because discrete types are treated separately in nominal_atoms

improved the code for showing that a type is in the pt-axclass (I try to slowly overcome my incompetence with such ML-code).

simp del: empty_Collect_eq;