[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

[Makarius]

On the sister thread 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00028.html
Henri mentions finite_UNIV.

Trying to reproduce the observed effects with Isabelle2012 vs. 
Isabelle/3155cee13c49 from today reveals a difference wrt. Phantom('a). 
The latter was introduced in Isabelle/f0ecc1550998 with an almost vacous 
log entry, and no coverage in NEWS nor CONTRIBUTORS.

What is its purpose?  Where is it documented?


 	Makarius