[isabelle-dev] erroneous "Legacy feature" warnings about secondary search path

[Brian Huffman]

Hello all,

I recently discovered that warnings about the secondard search path
are generated more often than they ought to be. I am using repository
version 1fa4725c4656.

Create two files A.thy and B.thy with the following contents:

theory A
imports "~~/src/HOL/Library/Cardinality"
begin
end

theory B
imports A
begin
end

Theory A loads an arbitrary file from HOL/Library, which is included
in the legacy default search path, although the full path is given
here to avoid the "Legacy feature" warning.

If I load theory A by itself in ProofGeneral, it imports
Cardinality.thy without warning. Similarly, if I load theory B by
itself in ProofGeneral, there is no warning. But if I have both A.thy
and B.thy open in ProofGeneral, step through A.thy first, and *then*
start stepping through B.thy, I get the following warning when I
import A from B:

### Legacy feature! File "Cardinality.thy" located via secondary
search path: "$ISABELLE_HOME/src/HOL/Library

Can anyone explain this behavior?

- Brian