# HG changeset patch
# User haftmann
# Date 1746626936 -7200
# Node ID 76262e8b53f7063ae9ff58e83ccf8818f42504c4
# Parent  6e3e59ac12c94e61a2047dc5f654abbb8bc2c982
prefer official precise attribute

diff -r 6e3e59ac12c9 -r 76262e8b53f7 src/HOL/Library/datatype_records.ML
--- a/src/HOL/Library/datatype_records.ML	Wed May 07 07:48:07 2025 +0200
+++ b/src/HOL/Library/datatype_records.ML	Wed May 07 16:08:56 2025 +0200
@@ -173,7 +173,7 @@
       end
 
     fun define name t =
-      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t))
+      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code equation]}),t))
       #> apfst (apsnd snd)
 
     val (updates, (lthy'', lthy')) =
diff -r 6e3e59ac12c9 -r 76262e8b53f7 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 07 07:48:07 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 07 16:08:56 2025 +0200
@@ -308,7 +308,7 @@
               |> Thm.close_derivation \<^here>
               |> singleton (Variable.export transfer_ctxt lthy4)
             val lthy5 = lthy4
-              |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
+              |> Local_Theory.note ((Binding.empty, @{attributes [code equation]}), [f_alt_def])
               |> snd
               (* if processing a mutual datatype (there is a cycle!) the corresponding quotient 
                  will be needed later and will be forgotten later *)
@@ -538,7 +538,7 @@
       |> singleton(Variable.export x_ctxt lthy6)
   in
     lthy6
-    |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code])
+    |> snd o Local_Theory.note ((Binding.empty, @{attributes [code equation]}), [rep_isom_code])
     |> Lifting_Setup.lifting_forget pointer
     |> pair (selss, diss, rep_isom_code)
   end