diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -210,7 +210,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 ([], [(P_var, P_inst), (x_var, x_inst)])
+      |> Thm.instantiate (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)])
       |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
       |> singleton (Variable.export ctxt' ctxt)
   in