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;