theory R
imports
  Main
begin

locale infinite =
  fixes bar :: "unit"

locale permutation_type = infinite "()" +
  fixes permute :: "('a \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b"
begin

definition eqvt :: "'b \<Rightarrow> bool" where
  "eqvt x \<longleftrightarrow> (\<forall>p. permute p x = x)"

end

definition permute_atom :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  "permute_atom p a = p a"

definition permute_bool :: "('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> bool" where
  "permute_bool p b = b"

context infinite
begin

sublocale atom_pt: permutation_type "permute_atom :: ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" .
sublocale bool_pt: permutation_type "permute_bool :: ('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> bool" .

term "atom_pt.eqvt"
term "bool_pt.eqvt"

(* everything is fine up to here *)
end

context infinite
begin

term "atom_pt.eqvt" (* this is visible *)
term "bool_pt.eqvt" (* but this is not *)

end

end