Changes

Summary

1. merged
2. more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
3. more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
4. support Export_Theory.read_proof, based on theory_name and serial;
5. clarified PThm: theory_name simplifies retrieval from exports;
6. Indexname.toString according to string_of_vname' in ML;
7. clarified type Indexname, with plain value Int; eliminated pointless cache_int;
8. more complete pattern match;
9. export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
10. support for (fully reconstructed) proof terms in Scala; proper cache_typs;
11. new material; rotated premises of Lim_transform_eventually