# HG changeset patch
# User wenzelm
# Date 1684861941 -7200
# Node ID 2ea20bb1493caae095d3325172606d8ae9549ef5
# Parent  838198d17a40e4972c33d2c5301d1140b421e11d
tuned: more antiquotations;

diff -r 838198d17a40 -r 2ea20bb1493c src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue May 23 18:59:19 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue May 23 19:12:21 2023 +0200
@@ -675,7 +675,7 @@
     lthy |>
     Local_Theory.notes (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
-          [Attrib.internal \<^here> (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
+          @{attributes [eqvt]}), [(ths, [])]))
       (names ~~ transp thss)) |> snd
   end;