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