# HG changeset patch
# User wenzelm
# Date 1631388370 -7200
# Node ID 39c98371606f222b5a3e3fe0fee7b5ef702e8bad
# Parent  b83fa8f3a271fb1f6ece2e9a91d5bd666f051fcc
tuned;

diff -r b83fa8f3a271 -r 39c98371606f src/HOL/Tools/record.ML
--- 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