theory Buggy
imports Main
begin

locale sub =
  fixes a :: 'a
begin
  definition P :: "'a \<Rightarrow> bool"
  where "P x \<equiv> True"
end

locale loc =
  X: sub a + Y: sub b
  for a and b +
  fixes f :: "'a \<Rightarrow> 'b"
  assumes "f a = b"
  (*
   * If the preceding line is removed, then constant "loc"
   * ends up having type "'a \<Rightarrow>'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool
   * instead of "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool
   *)

lemma
assumes "loc a b f" and "loc b c g"
shows "loc a c (g o f)"
proof
  interpret F: loc a b f using assms(1) by auto
  interpret G: loc b c g using assms(2) by auto
  have "\<And>x. F.X.P x" using F.X.P_def by auto
  have "\<And>x. G.X.P x" using G.X.P_def by auto
  (*
   * Constant G.X.P is unrecognized in the preceding line.
   * If the "interpret" lines are interchanged,
   * there is no error.
   *)
qed

end