berghofe [Thu, 01 Dec 2005 17:07:50 +0100] rev 18316
Improved norm_proof to handle proofs containing term (type) variables
with same name but different types (sorts): Offending term (type)
variables are replaced by dummy (T)Frees before applying the
substitution.