diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue May 23 18:46:15 2023 +0200
@@ -466,7 +466,7 @@
         val strong_raw_induct =
           mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
         val strong_induct_atts =
-          map (Attrib.internal o K)
+          map (Attrib.internal \<^here> o K)
             [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
           if length names > 1 then strong_raw_induct
@@ -484,8 +484,8 @@
         lthy2 |>
         Local_Theory.notes [((inducts_name, []),
           strong_inducts |> map (fn th => ([th],
-            [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
+            [Attrib.internal \<^here> (K ind_case_names),
+             Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;