Fuse strlit and implode in mlstringTheory

[myreen]

Currently, mlstringTheory defines a function implode as follows.

val implode_def = Define`
  implode = strlit`

which is exactly the same as the (only) constructor strlit for the mlstring type, which is defined in the same file as follows:

val _ = Datatype`mlstring = strlit string`

As discussed on Slack on 8 June 2018, it would be nice if strlit was renamed to implode in the definition of the mlstring type and implode_def was removed.

This requires going through the entire development replacing all mentions of strlit with implode and updating the translator to still produce good output for implode applied to a concrete string literal.

[mn200]

You could keep an overload in place to simplify your first task.

[tanyongkiam]

This should be an easy task but requires tweaking the translator slightly.