diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -209,7 +209,7 @@
          THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
          THEN CONVERSION (split_params_conv ctxt
            then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
-      |> Thm.instantiate (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)])
+      |> Thm.instantiate (TVars.empty, Vars.make2 (P_var, P_inst) (x_var, x_inst))
       |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
       |> singleton (Variable.export ctxt' ctxt)
   in