diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/record.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -1771,7 +1771,8 @@
       fun mk_eq_refl ctxt =
         @{thm equal_refl}
         |> Thm.instantiate
-          ([((("'a", 0), \<^sort>\<open>equal\<close>), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], [])
+          (TVars.make [((("'a", 0), \<^sort>\<open>equal\<close>), Thm.ctyp_of ctxt (Logic.varifyT_global extT))],
+           Vars.empty)
         |> Axclass.unoverload ctxt;
       val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
       val ensure_exhaustive_record =