cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer