[isabelle-dev] PolyML.makestring obsolete

[Makarius]

This is just a reminder of an important point that I am trying to make for 
many months already:

PolyML.makestring has no practical purpose outside bootstrapping of 
Isabelle/Pure.  Most people can forget that it ever existed.

The @{make_string} antiquotation does a better job, with proper pretty 
printing and formal markup.  It is officially documented in the 
"implementation" manual, including its inherent undefinedness of the 
precise output.

Printing of internal ML values is for debugging, not for actual 
application code, so it is better not committed at all.  (Application code 
with lots of optional debugging functionality routinely breaks down when 
that is enabled.)


 	Makarius