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