tuning

compile

cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)

improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well

removed needless function that duplicated standard functionality, with a little unnecessary twist

removed more dead code

be a bit more liberal with respect to the universal sort -- it sometimes help

renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"

merged