[isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?

[Lukas Bulwahn]

Hi Florian,

in the changeset e8400e31528a of the Isabelle repository, you moved the 
theorem Pair_inject in the Product_Type theory into a section called 
"Legacy theorem bindings and duplicates".

In my current development, I rely on the theorem Pair_inject, and it is 
the most suitable rule for my purpose.
Why was it considered legacy or a duplicate? Does this still hold at the 
current tip?

NB: At the current tip d7917ec16288, I cannot find any duplicate theorem 
for Pair_inject.


Lukas