isabelle - イザベル: メティス: プルーフ状態にはユニバーサル ソート {} が含まれています

Question

Metisは私に警告を出します：

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

この警告はどういう意味ですか? これは、メティスプルーフが警告なしよりも「音が少ない」ことを示していますか?