# HG changeset patch
# User wenzelm
# Date 1703275396 -3600
# Node ID 032a31db4c6f371befb8915fdfe32814b55e568e
# Parent  6d167422bcb058027bb29e5f6a1a1da8e0ac7319
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;

diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- 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 *)
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/HOLCF/ex/Pattern_Match.thy
--- 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;
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Import/import_rule.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Library/old_recdef.ML
--- 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;
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Nominal/nominal_atoms.ML
--- 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 *)
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Nominal/nominal_datatype.ML
--- 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'))))))
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- 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) =
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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))
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- 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'))
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Tools/choice_specification.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Tools/record.ML
--- 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;
 
diff -r 6d167422bcb0 -r 032a31db4c6f src/HOL/Types_To_Sets/unoverload_def.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/Isar/expression.ML
--- 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
diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/Proof/extraction.ML
--- 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)])
diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/axclass.ML
--- 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);
 
diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/global_theory.ML
--- 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;
 
diff -r 6d167422bcb0 -r 032a31db4c6f src/Pure/pure_thy.ML
--- 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;
diff -r 6d167422bcb0 -r 032a31db4c6f src/ZF/Tools/datatype_package.ML
--- 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;
 
diff -r 6d167422bcb0 -r 032a31db4c6f src/ZF/Tools/inductive_package.ML
--- 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*)
diff -r 6d167422bcb0 -r 032a31db4c6f src/ZF/Tools/primrec_package.ML
--- 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 =