update some lem-generated files

latest lem now produces fewer unnecessary parentheses
fix up a proof

a case is no longer needed, due (I think) to new automatic rewrites
being added to HOL recently
use the new compset fragments in combin,pair,finite_map
ml_repl_step cheats removed

I realised that sets are used in the inferencer. These
sets really ought to be sptrees or some other binary
trees, since, as it currently stands, HOL sets translate
into functions in CakeML.
use new computeLib.add_datatype_info
update compile_primitivesTheory for recent additions to HOL
remove MAP2_def from cakeml compset, should already be in list_rws

actually list_rws contains MAP2 which doesn't cover cases where it is
applied to lists of unequal lengths, but those shouldn't be relevant.
move some theorems into miscTheory
use new compset fragment in HOL's examples/parsing
generate smaller Theory.sig for ml_repl_step
update sideTheory

not sure if things need to be added to it, but repl_step_side is proved
(and dependencies).
some new Lem-generated files

this slightly broke one proof due to a change of bound variable names
remove probably useless bring_to_front_overload"Num" from cakeml_compute

I didn't see any occurrences of "Num" in the file, so I presume this
isn't necessary any more. If it is, it should be the temp_ version since
this is not a script file.
make dependence on $HOLDIR/examples/parsing explicit

for pegLib which is used in cakeml_computeLib

this might be picked up transitively (through heaps) via the dependence
on ../parsing, but that seems to be a bit flaky
start updating bootstrap/Holmakefile

this commit makes it something more reasonable given all the changes
since bootstrap was last touched, although it may still need further
tweaking
tidy use of SUC_TO_NUMERAL_DEFN_CONV in cakeml_computeLib
use sLet_pat_thm rather than _def in cakeml_computeLib

the former is a small simple definition, whereas the definition has
unwieldy pattern-matching. probably the nice theorem should move into
compilerTermination or something so it doesn't depend on the proofs, but
this works for now.
move sLet_pat_thm into compilerTerminationTheory
save theorems precomputing evaluation of real_inst_length together

previously had generated a separate theorem for each case and added them
to the_compset. it makes more sense to save a single theorem (the
conjunction) so it's easier to find it to add it to other compsets.
use eval_real_inst_length for code_labels_conv in cakeml_compute

labels_computeLib.code_labels_conv needs a conversion to evaluate the
length function. previously had been passing in the cakeml compset
evaluator, but this doesn't include evaluation of real_inst_length. it
actually probably makes more sense to use a conversion that is
specialised to evaluating real_inst_length, so that is what we do in
this commit. if it needs to become more versatile later (e.g. for other
instruction lengths) we could make eval_real_inst_length a reference.