moved name space externalization flags back to name_space.ML; added pure version extern_flags; do not export internal get_accesses;

moved name space externalization flags back to name_space.ML; display: always show prefix for now; tuned signature;

reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

merged

Thm.binding;

added type binding and val empty_binding;

updated generated files;