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;

slightly more abstract data handling in Fast_Lin_Arith;

theory data merge: prefer left side uniformly;

tuned;

simplification/standardization of some theory data;

misc tuning and simplification, notably theory data;