Changes

Summary

1. more efficient data structure;
2. clarified signature;
3. guard constraints by record_proofs=1, until performance implications have become more clear;
4. more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;
5. tuned;
6. tuned;
7. maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms; tuned;
8. more direct proofs for type classes; misc tuning and cleanup;
9. tuned;
10. clarified modules: inference kernel maintains sort algebra within the logic;
11. more elementary treatment of standard_vars (unconstrainT is already standard);
12. clarified module structure;
13. simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);
14. abstract type theory_id -- ensure non-equality type independently of implementation;