misc tuning;

more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;

more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses;

minor performance tuning: more compact representation of only sparsely table;

minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;

proper checks;

tuned;

tuned structure;

tuned signature;

tuned;