--- a/src/HOL/Import/import_rule.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/HOL/Import/import_rule.ML Sun Dec 01 14:01:47 2024 +0100
@@ -335,7 +335,7 @@
val thm = Drule.export_without_context_open thm
val tvs = Term.add_tvars (Thm.prop_of thm) []
val tns = map (fn (_, _) => "'") tvs
- val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
+ val nms = Name.variants (Variable.names_of ctxt) tns
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
in