Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...

added simplification meta rules;

standard congs;

Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.

Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).

Uses new version of Datatype.occs_in_prems

auto update