[CakeML-Dev] case expressions with set_grammar_ancestry

[Michael.Norrish at data61.csiro.au]

If grammar ancestry is set with the set_grammar_ancestry function in a script file, then case expressions won’t pretty-print properly (they’ll print with the underlying constants, e.g., option_CASES 1 (\n. n + 1)). I’ll fix this in HOL soon, but if you encounter this, the workaround is straightforward: use 

  temp_overload_on(“case”, ``option_CASE``)

for ``option_CASE``, ``pair_CASE``, ``list_CASE`` etc. 

Note that there is no issue if an ancestor has used set_grammar_ancestry, but your current script file does not.

Michael