--- a/src/HOL/Tools/Function/pattern_split.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -20,7 +20,7 @@
 
 fun new_var ctxt vs T =
   let
-    val [v] = Variable.variant_frees ctxt vs [("v", T)]
+    val v = singleton (Variable.variant_names (fold Variable.declare_names vs ctxt)) ("v", T)
   in
     (Free v :: vs, Free v)
   end