src/HOL/Tools/record.ML

         rewrite_rule (Proof_Context.init_global thy)
           [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
       fun mk_eq_refl thy =
         @{thm equal_refl}
         |> Thm.instantiate
-          ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
+          ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], [])
         |> Axclass.unoverload thy;
       val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
       val ensure_exhaustive_record =
         ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
     in