clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Dec 22 21:03:16 2023 +0100
@@ -87,8 +87,7 @@
fun mk_def c (b, t, _) =
(Thm.def_binding b, Logic.mk_equals (c, t))
val defs = map2 mk_def consts specs
- val (def_thms, thy) =
- Global_Theory.add_defs false (map Thm.no_attributes defs) thy
+ val (def_thms, thy) = fold_map Global_Theory.add_def defs thy
in
((consts, def_thms), thy)
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Dec 22 21:03:16 2023 +0100
@@ -300,8 +300,7 @@
val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs)
in
val (bisim_def_thm, thy) = thy |>
- yield_singleton (Global_Theory.add_defs false)
- ((Binding.qualify_name true comp_dbind "bisim_def", bisim_eqn), [])
+ Global_Theory.add_def (Binding.qualify_name true comp_dbind "bisim_def", bisim_eqn)
end (* local *)
(* prove coinduction lemma *)
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Dec 22 21:03:16 2023 +0100
@@ -128,8 +128,7 @@
(* register constant definitions *)
val (fixdef_thms, thy) =
- (Global_Theory.add_defs false o map Thm.no_attributes)
- (map Thm.def_binding binds ~~ eqns) thy
+ fold_map Global_Theory.add_def (map Thm.def_binding binds ~~ eqns) thy
(* prove applied version of definitions *)
fun prove_proj (lhs, rhs) =
@@ -212,8 +211,8 @@
val typ = Term.fastype_of rhs
val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
val eqn = Logic.mk_equals (const, rhs)
- val def = Thm.no_attributes (Thm.def_binding bind, eqn)
- val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
+ val def = (Thm.def_binding bind, eqn)
+ val (def_thm, thy) = Global_Theory.add_def def thy
in
((const, def_thm), thy)
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Dec 22 21:03:16 2023 +0100
@@ -186,8 +186,7 @@
(******************************************************************************)
fun add_qualified_def name (dbind, eqn) =
- yield_singleton (Global_Theory.add_defs false)
- ((Binding.qualify_name true dbind name, eqn), [])
+ Global_Theory.add_def (Binding.qualify_name true dbind name, eqn)
fun add_qualified_thm name (dbind, thm) =
yield_singleton Global_Theory.add_thms
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 22 21:03:16 2023 +0100
@@ -397,8 +397,7 @@
fun mk_def c (b, t, mx) =
(Thm.def_binding b, Logic.mk_equals (c, t));
val defs = map2 mk_def consts specs;
- val (def_thms, thy) =
- Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
+ val (def_thms, thy) = fold_map Global_Theory.add_def defs thy;
in
((consts, def_thms), thy)
end;
--- a/src/HOL/Import/import_rule.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Dec 22 21:03:16 2023 +0100
@@ -172,9 +172,8 @@
val constbinding = Binding.name constname
val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
- val (thms, thy2) = Global_Theory.add_defs false
- [((Binding.suffix_name "_hldef" constbinding, eq), [])] thy1
- val def_thm = freezeT thy1 (hd thms)
+ val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" constbinding, eq) thy1
+ val def_thm = freezeT thy1 thm
in
(meta_eq_to_obj_eq def_thm, thy2)
end
--- a/src/HOL/Library/old_recdef.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Library/old_recdef.ML Fri Dec 22 21:03:16 2023 +0100
@@ -2011,8 +2011,7 @@
val def_name = Thm.def_name (Long_Name.base_name fid)
val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
val def_term = const_def thy (fid, Ty, wfrec_R_M)
- val ([def], thy') =
- Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
+ val (def, thy') = Global_Theory.add_def (Binding.name def_name, def_term) thy
in (def, thy') end;
end;
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Dec 22 21:03:16 2023 +0100
@@ -193,8 +193,7 @@
[(Binding.name swap_name, SOME swapT, NoSyn)]
[((Binding.empty_atts, def1), [], [])] ||>
Sign.parent_path ||>>
- Global_Theory.add_defs_unchecked true
- [((Binding.name name, def2), [])] |>> (snd o fst)
+ fold_map Global_Theory.add_def_unchecked_overloaded [(Binding.name name, def2)] |>> (snd o fst)
end) ak_names_types thy1;
(* declares a permutation function for every atom-kind acting *)
@@ -253,7 +252,7 @@
val def = Logic.mk_equals
(cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
in
- Global_Theory.add_defs_unchecked true [((Binding.name name, def), [])] thy'''
+ Global_Theory.add_def_unchecked_overloaded (Binding.name name, def) thy'''
end) ak_names_types thy) ak_names_types thy4;
(* proves that every atom-kind is an instance of at *)
--- 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'))))))
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Dec 22 21:03:16 2023 +0100
@@ -243,7 +243,7 @@
|> Sign.add_consts (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (Global_Theory.add_defs false o map Thm.no_attributes)
+ |> fold_map Global_Theory.add_def
(map
(fn ((((name, comb), set), T), T') =>
(Binding.name (Thm.def_name (Long_Name.base_name name)),
@@ -335,10 +335,10 @@
fold_rev lambda fns1
(list_comb (reccomb,
flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
- val ([def_thm], thy') =
+ val (def_thm, thy') =
thy
|> Sign.declare_const_global decl |> snd
- |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
+ |> Global_Theory.add_def def;
in (defs @ [def_thm], thy') end;
val (case_defs, thy2) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 22 21:03:16 2023 +0100
@@ -1144,9 +1144,9 @@
(list_comb (Const (name, T), args))))
val lhs = Const (mode_cname, funT)
val def = Logic.mk_equals (lhs, predterm)
- val ([definition], thy') = thy |>
+ val (definition, thy') = thy |>
Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
- Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
+ Global_Theory.add_def (Binding.name (Thm.def_name mode_cbasename), def)
val ctxt' = Proof_Context.init_global thy'
val rules as ((intro, elim), _) =
create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Dec 22 21:03:16 2023 +0100
@@ -86,9 +86,9 @@
val constT = map fastype_of (params @ args) ---> HOLogic.boolT
val lhs = list_comb (Const (full_constname, constT), params @ args)
val def = Logic.mk_equals (lhs, atom)
- val ([definition], thy') = thy
+ val (definition, thy') = thy
|> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
+ |> Global_Theory.add_def (Binding.name (Thm.def_name constname), def)
in
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
@@ -240,9 +240,9 @@
val const = Const (full_constname, constT)
val lhs = list_comb (const, frees)
val def = Logic.mk_equals (lhs, abs_arg')
- val ([definition], thy') = thy
+ val (definition, thy') = thy
|> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
+ |> Global_Theory.add_def (Binding.name (Thm.def_name constname), def)
in
(list_comb (Logic.varify_global const, vars),
((full_constname, [definition])::new_defs, thy'))
--- a/src/HOL/Tools/choice_specification.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML Fri Dec 22 21:03:16 2023 +0100
@@ -28,9 +28,10 @@
else thname
val def_eq =
Logic.mk_equals (Const (cname_full, ctype), HOLogic.choice_const ctype $ P)
- val (thms, thy') =
- Global_Theory.add_defs covld [((Binding.name cdefname, def_eq), [])] thy
- val thm' = [thm,hd thms] MRS @{thm exE_some}
+ val (def_thm, thy') =
+ (if covld then Global_Theory.add_def_overloaded else Global_Theory.add_def)
+ (Binding.name cdefname, def_eq) thy
+ val thm' = [thm, def_thm] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
end
--- a/src/HOL/Tools/record.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/record.ML Fri Dec 22 21:03:16 2023 +0100
@@ -138,11 +138,11 @@
val isom_name = Sign.full_name typ_thy isom_binding;
val isom = Const (isom_name, isomT);
- val ([isom_def], cdef_thy) =
+ val (isom_def, cdef_thy) =
typ_thy
|> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
- |> Global_Theory.add_defs false
- [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
+ |> Global_Theory.add_def
+ (Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body))
val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
val cons = \<^Const>\<open>iso_tuple_cons absT leftT rightT\<close>;
@@ -1594,10 +1594,10 @@
fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
- val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () =>
+ val (ext_def, defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () =>
typ_thy
|> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
- |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]);
+ |> Global_Theory.add_def (Thm.def_binding ext_binding, ext_spec));
val defs_ctxt = Proof_Context.init_global defs_thy;
@@ -2060,12 +2060,9 @@
(sel_decls ~~ (field_syntax @ [NoSyn]))
|> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
- |> (Global_Theory.add_defs false o
- map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
- ||>> (Global_Theory.add_defs false o
- map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
- ||>> (Global_Theory.add_defs false o
- map (Thm.no_attributes o apfst (Binding.concealed o Binding.name)))
+ |> fold_map (Global_Theory.add_def o apfst (Binding.concealed o Binding.name)) sel_specs
+ ||>> fold_map (Global_Theory.add_def o apfst (Binding.concealed o Binding.name)) upd_specs
+ ||>> fold_map (Global_Theory.add_def o apfst (Binding.concealed o Binding.name))
[make_spec, fields_spec, extend_spec, truncate_spec]);
val defs_ctxt = Proof_Context.init_global defs_thy;
--- a/src/HOL/Types_To_Sets/unoverload_def.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Types_To_Sets/unoverload_def.ML Fri Dec 22 21:03:16 2023 +0100
@@ -37,9 +37,8 @@
val (with_const, thy') = Sign.declare_const_global
((binding_with, Term.fastype_of rhs_abs'), NoSyn)
thy
- val ([with_def], thy'') = Global_Theory.add_defs false
- [((Binding.suffix_name "_def" binding_with,
- Logic.mk_equals (with_const, rhs_abs')), [])] thy'
+ val (with_def, thy'') = Global_Theory.add_def
+ (Binding.suffix_name "_def" binding_with, Logic.mk_equals (with_const, rhs_abs')) thy'
val with_var_def =
fold_rev
--- a/src/Pure/Isar/expression.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/Isar/expression.ML Fri Dec 22 21:03:16 2023 +0100
@@ -707,11 +707,11 @@
val head = Term.list_comb (Const (name, predT), args);
val statement = Object_Logic.ensure_propT thy_ctxt head;
- val ([pred_def], defs_thy) =
+ val (pred_def, defs_thy) =
thy
|> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
|> Sign.declare_const_global ((binding, predT), NoSyn) |> snd
- |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])];
+ |> Global_Theory.add_def (Thm.def_binding binding, Logic.mk_equals (head, body));
val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
val intro = Goal.prove_global defs_thy [] norm_ts statement
--- a/src/Pure/Proof/extraction.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Dec 22 21:03:16 2023 +0100
@@ -820,10 +820,9 @@
in
thy
|> Sign.add_consts [(b, fastype_of ft, NoSyn)]
- |> Global_Theory.add_defs false
- [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
- Logic.mk_equals (head, ft)), [])]
- |-> (fn [def_thm] =>
+ |> Global_Theory.add_def
+ (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+ |-> (fn def_thm =>
Spec_Rules.add_global b Spec_Rules.equational
[Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
#> Code.declare_default_eqns_global [(def_thm, true)])
--- a/src/Pure/axclass.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/axclass.ML Fri Dec 22 21:03:16 2023 +0100
@@ -394,10 +394,10 @@
val class_eq =
Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
- val ([def], def_thy) =
+ val (def, def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])];
+ |> Global_Theory.add_def (Thm.def_binding bconst, class_eq);
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
--- a/src/Pure/global_theory.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/global_theory.ML Fri Dec 22 21:03:16 2023 +0100
@@ -49,10 +49,10 @@
(string * thm list) * theory
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> theory ->
(string * thm list) list * theory
- val add_defs: bool -> ((binding * term) * attribute list) list ->
- theory -> thm list * theory
- val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
- theory -> thm list * theory
+ val add_def: binding * term -> theory -> thm * theory
+ val add_def_overloaded: binding * term -> theory -> thm * theory
+ val add_def_unchecked: binding * term -> theory -> thm * theory
+ val add_def_unchecked_overloaded: binding * term -> theory -> thm * theory
end;
structure Global_Theory: GLOBAL_THEORY =
@@ -374,7 +374,7 @@
local
-fun add unchecked overloaded = fold_map (fn ((b, prop), atts) => fn thy =>
+fun add unchecked overloaded (b, prop) thy =
let
val context = Defs.global_context thy;
val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
@@ -382,12 +382,14 @@
|> Thm.forall_intr_frees
|> Thm.forall_elim_vars 0
|> Thm.varifyT_global;
- in thy' |> apply_facts unnamed official2 (b, [([thm], atts)]) |>> the_single end);
+ in thy' |> apply_facts unnamed official2 (b, [([thm], [])]) |>> the_single end;
in
-val add_defs = add false;
-val add_defs_unchecked = add true;
+val add_def = add false false;
+val add_def_overloaded = add false true;
+val add_def_unchecked = add true false;
+val add_def_unchecked_overloaded = add true true;
end;
--- a/src/Pure/pure_thy.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/Pure/pure_thy.ML Fri Dec 22 21:03:16 2023 +0100
@@ -225,7 +225,7 @@
(qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),
(qualify (Binding.make ("conjunction", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", NoSyn)]
#> Sign.local_path
- #> (Global_Theory.add_defs false o map Thm.no_attributes)
+ #> fold (snd oo Global_Theory.add_def)
[(Binding.make ("prop_def", \<^here>),
prop "(CONST Pure.prop :: prop \<Rightarrow> prop) (A::prop) \<equiv> A::prop"),
(Binding.make ("term_def", \<^here>),
@@ -234,7 +234,7 @@
prop "(CONST Pure.sort_constraint :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself) \<equiv>\
\ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"),
(Binding.make ("conjunction_def", \<^here>),
- prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd
+ prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")]
#> fold (#2 oo Thm.add_axiom_global) Theory.equality_axioms);
end;
--- a/src/ZF/Tools/datatype_package.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/ZF/Tools/datatype_package.ML Fri Dec 22 21:03:16 2023 +0100
@@ -242,17 +242,16 @@
if need_recursor then
thy
|> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
- |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
+ |> Global_Theory.add_def (apfst Binding.name recursor_def) |> #2
else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts
(map (fn (c, T, mx) => (Binding.name c, T, mx))
((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
- |> Global_Theory.add_defs false
- (map (Thm.no_attributes o apfst Binding.name)
+ |> fold_map (Global_Theory.add_def o apfst Binding.name)
(case_def ::
- flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
+ flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))
||> add_recursor
||> Sign.parent_path;
--- a/src/ZF/Tools/inductive_package.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/ZF/Tools/inductive_package.ML Fri Dec 22 21:03:16 2023 +0100
@@ -168,10 +168,10 @@
else ()
(*add definitions of the inductive sets*)
- val (_, thy1) =
+ val thy1 =
thy0
|> Sign.add_path big_rec_base_name
- |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
+ |> fold (snd oo Global_Theory.add_def o apfst Binding.name) axpairs;
(*fetch fp definitions from the theory*)
--- a/src/ZF/Tools/primrec_package.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/ZF/Tools/primrec_package.ML Fri Dec 22 21:03:16 2023 +0100
@@ -167,9 +167,9 @@
List.foldr (process_eqn thy) NONE eqn_terms;
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
- val ([def_thm], thy1) = thy
+ val (def_thm, thy1) = thy
|> Sign.add_path (Long_Name.base_name fname)
- |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
+ |> Global_Theory.add_def (apfst Binding.name def);
val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info)
val eqn_thms0 =