theory Scratch
  imports Main
begin

ML \<open>val theory_naming = Sign.naming_of @{theory}\<close>
setup \<open>Sign.map_naming Name_Space.concealed\<close>

definition "foo x = x"

lemma aaa: "foo (foo x) = x"
  by (simp add: foo_def)

find_theorems name: aaa

setup \<open>Sign.map_naming (K theory_naming)\<close>

lemma bbb: "foo (foo (foo x)) = x"
  by (simp add: foo_def)

find_theorems name: bbb

end