tuned

proper context for various Thy_Output options, via official configuration options in ML and Isar;

Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);

eliminated old 'local' command;

more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;