--- 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