Isabelle: Metis: Proof state contains the universal sort {}

Question

Metis gives me the warning:

Metis: Proof state contains the universal sort {} 
("HOL/Tools/Metis/metis_tactic.ML")

What does this warning mean? Is this an indication that the metis proof is "less sound" than without the warning?

Answer 1

The proof is definitely sound. As I recall, this message is mainly of value to developers, for helping to diagnose why a metis call would fail. Normal HOL goals do not contain empty sorts.

My guess is that this warning is obsolete.