diff -r 878bc24681d9 -r 1bfad73ab115 src/HOL/Import/import_rule.ML
--- 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