just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;

added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);

tuned;

removed unused "option" variants of "same" operations;

more basic replacement of newlines;

static Symbol.spaces;

proper use of var stopped;

removed junk;

tuned headers;

tuned;