Possible pretty-printing overload issue

[mn200]

See CakeML commit 32eda18 and

To reproduce, checkout that commit, go to hol-light/standard/syntax and build holSyntaxTheory, then get holSyntaxExtraScript through HOL down to proves_term_ok. Then put the theorem in proves_term_ok onto your goal stack.

From Scott Owens

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.