Could we use the agents to clean up lib code to use Syntax defs?

There are (still) heaps of places where a lib file does some parsing or other hack to avoid going through the standard boilerplate of setting up or using a Syntax module.

In the worst cases, the code is making fragile use of parsing and `mk_icomb` when a relevant Syntax module exists.

I wrote this kind of patch this afternoon, and it's boring. Could we fire up the LLM agents to go looking for these kinds of things and patch them up? It seems it would be easy to check that they're not breaking anything.

Here's the example patch I wrote by hand:

https://github.com/talsewell/cakeml/commit/b5d7bde40baa6be0d35f1c257bcadcc99ca0bb6f

It's fixing up the monadic translator libs to stop doing things like this:
```
val SOME_const = “SOME”
val one_const = “1 : num”
```
And to instead prefer things like `numSyntax.term_of_int 1` and `optionSyntax.mk_some`.