merged

more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);

more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;