--- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Dec 22 21:03:16 2023 +0100
@@ -595,14 +595,14 @@
(TFree (singleton (Name.variant_list (map fst tvs)) "'a", \<^sort>\<open>type\<close>));
val pi = Free ("pi", permT);
val T = Type (Sign.full_name thy name, map TFree tvs);
- in apfst (pair r o hd)
- (Global_Theory.add_defs_unchecked true
- [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
+ in apfst (pair r)
+ (Global_Theory.add_def_unchecked_overloaded
+ (Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
(Const (\<^const_name>\<open>Nominal.perm\<close>, permT --> T --> T) $ pi $ Free ("x", T),
Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
(Const (\<^const_name>\<open>Nominal.perm\<close>, permT --> U --> U) $ pi $
(Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
- Free ("x", T))))), [])] thy)
+ Free ("x", T))))) thy)
end))
(types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
@@ -775,9 +775,9 @@
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (rep_name, T --> T') $ lhs, rhs));
val def_name = (Long_Name.base_name cname) ^ "_def";
- val ([def_thm], thy') = thy |>
+ val (def_thm, thy') = thy |>
Sign.add_consts [(cname', constrT, mx)] |>
- (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
+ Global_Theory.add_def (Binding.name def_name, def);
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
fun dt_constr_defs ((((((_, (_, _, constrs)),
@@ -2040,7 +2040,7 @@
|> Sign.add_consts (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+ |> fold_map Global_Theory.add_def (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T)
(Const (\<^const_name>\<open>The\<close>, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
(set $ Free ("x", T) $ Free ("y", T'))))))