--- 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;