pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);

more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;

Syntax.read thy;

tuned sort_ord: pointer_eq; tuned size_of_term: less stack usage;

removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort; added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);

eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;

replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);

added implies_intr_hyps (from thm.ML);

added joinable;

stylistic improvements