Adjust grammars, proofs to handle "nil" as a constructor name.

Also fix up constructor names that are qualified with a structure
name, allowing one to write List.nil and have it recognised as
something that might appear in a pattern, for example.
further progress on Equal
rec Equal verified
printing of ASTs is now an opt-in feature
avoids generating empty names
translator now proves check_ctors_decs
got HOL light example running again -- was out of date
translator now avoids duplicate constructor names
translator uses lists (nil and ::) from init_envC
move some things in miscLib back into HOL
tweak miscLib.discharge_hyps tactic
make regression-test print the HOL rev and machine info
Merge remote-tracking branch 'origin/x64'

Conflicts:
	translator/ml_translatorLib.sml