tuned;

--- a/src/HOL/Tools/record.ML	Sat Sep 11 21:16:23 2021 +0200
+++ b/src/HOL/Tools/record.ML	Sat Sep 11 21:26:10 2021 +0200
@@ -1781,8 +1781,7 @@
           val ctxt = Proof_Context.init_global thy;
         in
           thy
-          |> Code.declare_default_eqns_global
-               [(mk_eq (Proof_Context.init_global thy) eq_def, true), (mk_eq_refl (Proof_Context.init_global thy), false)]
+          |> Code.declare_default_eqns_global [(mk_eq ctxt eq_def, true), (mk_eq_refl ctxt, false)]
         end;
     in
       thy