tuned: more antiquotations;
authorwenzelm
Tue, 23 May 2023 19:12:21 +0200
changeset 78097 2ea20bb1493c
parent 78096 838198d17a40
child 78098 2cd7e5518d0d
tuned: more antiquotations;
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;