pretty_thm_aux etc.: explicit show_status flag;

simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;

@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;

tuned;