remove some unnecessary termination proofs

lem can be coaxed into emitting a call to Define that can do an
automatic termination proof. only looked at stuff under compiler/ so far
for this, but it is probably applicable elsewhere.
remove an unused variable in bytecode.lem
make zero_vars_* in compilerTermination temporary
fix compiler tests for printing of types

n.b. not actually testing the printing of types (since I don't want to
construct the map from declarations to type names, which type inference
would provide), just working around it.
delete GENLIST_NIL

close enough to existing already as listTheory.NULL_GENLIST
minor fix to compilerProofsTheory

since remove_mat_var lost its termination proof (and hence its
redefinition in compilerTerminationTheory).
std_prelude translates toString
prove a cheat in hol_verificationScript.sml
strengthen holSemantics.proves_IMP

add Const n (typeof t) to deftm (Constdef n t); this gives a somewhat
quick route to showing that defined constants in an ok context are
term_ok. (not sure if such a route didn't already exist.)
prove another hol_verificationScript.sml cheat
use capital A type variable for Equal/Select

to be consistent with the aty abbreviation defined in
hol_verificationScript.sml (and with the HOL Light convention...)
clean up header of hol_verificationScript.sml

make it nicer for vim mode and vim's (broken) syntax highlighting for
SML
prove another cheat in hol_verificationScript.sml
prove another cheat in hol_verificationScript.sml
reinserted definition of zBC_LoadRev
added missing definition to compileReplDecsCheatScript
commented out remove_mat_var -- does this still exist?
lemma that might help in eval of x64_code
prove cheat in hol_verificationScript.sml

had to add an assumption to the statement
uncapitalise reference to PrinterTheory in x64_heapScript.sml