Following a discussion with Michael Färber (Dedukteam, Paris/Cachan), proof term export in Isabelle/910a081cca74 does not handle hidden polymorphism within the proof term. Example: Lattices_Big.semilattice_set.infinite where a spurious type variable ?'a123 becomes an external 'b, without a corresponding type application in its use elsewhere.

A better approach is to use techniques from strip_shyps to "ground" such stray type variables, and not invent new type arguments.