theory Bar
imports Main Foo
begin

  context L
  begin
    definition bar where "bar = False"
  end

  interpretation Foobar: L .

  (* With interpretation in Foo.thy commented this fails -- expected. *)
  (* With interpretation in Foo.thy uncommented this succeeds -- expected. *)
  lemma "Foo.foo = True" using Foo.foo_def by auto

  (* With interpretation in Foo.thy commented out these succeed -- expected. *)
  (* With interpretation in Foo.thy uncommented these fail -- strange. *)
  lemma "Foobar.foo = True" using Foobar.foo_def by auto
  lemma "Foobar.bar = False" using Foobar.bar_def by auto

  (* This fails regardless -- strange. *)
  lemma "Foo.bar = False" using Foo.bar_def by auto

end