Changes

Summary

1. proper message (amending 94442fce40a5);
2. more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
3. uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;
4. tuned;
5. updated xml_size;
6. prefer named result;
7. more robust expose_proofs corresponding to register_proofs/consolidate_theory; expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;