amended to unoverload actually all parameters of a type variable
restore type variable names in unoverload_type --HG-- extra : rebase_source : 5bebe9c7a6774e498f5c496fcd7ff8b9b932efb0
isabelle update -u control_cartouches;
tuned exception
restructured
result of unoverload is not in normal form
tuned
allow for a list of vars
parse var
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
a derived rule combining unoverload and internalize_sort