HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input;
added check_tvar, check_tfree convenience;
tuned;

modernized treatment of sort constraints in specification;
pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;

typecopy: observe given sort constraints more precisely;

inline old Record.read_typ/cert_typ;
spelling;

spelling;