# [isabelle] Interpreting a locale on it's own underlying definitions

`I'm trying to ensure that any theorem attributes given in a locale are
``propagated to the locale's underlying global definitions. Here's an
``example:
`
locale L =
fixes a :: int
begin
definition
x :: int where
"x = a"
lemma r[simp]: "x + a = 2 * a"
by (simp add: x_def)
end
interpretation L [a] .

`I then use the interpretation command above to ensure that the simp
``rule "r" in L is installed for the locale's underlying global
``definition L.x. This works, but with an unintended side-effect: The
``definition of f below causes a type error, because the interpretation
``command has also installed the unqualified name "x" into the namespace.
`
definition
f :: "('a \<Rightarrow> 'a)" where
"f x = foo"

`How can I perform a locale interpretation that targets the current
``background theory, but that doesn't add the unqualified names of the
``locale definitions to the background theory? Note that some of these
``definitions may occur after the original interpretation command.
`
Thanks,
-john

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*