corrected typo introduced by me

now obsolete

moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions

Exporting curried versions of tail recursive equations instead of internal ones

proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);

removed non-modular comment;

interpretation: attempt to be more serious about name_morphism;