[isabelle] Predicate_Compile.present_graph

In Isabelle2014, Isabelle/ML structure »Predicate_Compile«, there is a
quasi-option as low-level unsynchronized reference »present_graph«,
which allows to display some kind of dependency graph during a run of
the predicate compiler. It does neither appear in documentation nor in
source. Is there any real application of this?

The reason why I am asking is that this would need significant
de-obscurification and modernization to stay in the middle run, and
efforts could be saved by just dropping it silently.

Looking forward to your suggestions,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.