[CakeML-dev] bad merge on env-refactor

[Michael.Norrish at data61.csiro.au]

The merge at 45b1b32 has messed with the work I did in d2a43ca, and has also created some very bad definitions.  The former is not so important, but the latter is disastrous. 

In particular, you can’t write

  dtcase x of 
    [Lf (TK LbrackT,_); Lf (TK RbrackT,_)] =>

and similar because it causes an immense blow up in the size of the definition (every possible token constructor gets involved). If we were using PMATCH for these, that would be a different thing…  I don’t know what the plan is for use of PMATCH right now, but if I’m to fix the proofs directory, I’m going to revert aa09475’s changes to cmlPtreeConversionScript.sml.

Michael