The Isabelle/HOL record package is a leftover from ancient global-theory specification era. It should be properly localized, but this is difficult due to special features that have accumulated over time; some are required in special applications, some might be superfluous.

It will require substantial research and development to sort this out.