more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;

--- a/src/Pure/Isar/proof_context.ML	Wed Dec 27 15:57:42 2023 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Dec 27 16:10:10 2023 +0100
@@ -1053,9 +1053,9 @@
   let
     val name_pos = full_name_pos ctxt b;
     fun app_fact (thms, atts) =
-      fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts)))
-        (Global_Theory.name_thms Global_Theory.unofficial1 name_pos thms);
-    val (thms', ctxt') = fold_maps app_fact facts ctxt;
+      fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) thms;
+    val (thms', ctxt') =
+      fold_maps app_fact (Global_Theory.name_facts Global_Theory.unofficial1 name_pos facts) ctxt;
     val thms'' = Global_Theory.name_thms Global_Theory.unofficial2 name_pos thms';
     val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms'');
   in ((#1 name_pos, thms''), ctxt'') end;

--- a/src/Pure/global_theory.ML	Wed Dec 27 15:57:42 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 16:10:10 2023 +0100
@@ -31,6 +31,7 @@
   val unofficial2: name_flags
   val name_thm: name_flags -> string * Position.T -> thm -> thm
   val name_thms: name_flags -> string * Position.T -> thm list -> thm list
+  val name_facts: name_flags -> string * Position.T -> (thm list * 'a) list -> (thm list * 'a) list
   val check_thms_lazy: thm list lazy -> thm list lazy
   val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
   val store_thm: binding * thm -> theory -> thm * theory
@@ -253,6 +254,10 @@
   Thm_Name.list name_pos thms
   |> map (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
 
+fun name_facts name_flags name_pos facts =
+  Thm_Name.expr name_pos facts
+  |> (map o apfst o map) (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
+
 end;
 
 
@@ -314,7 +319,7 @@
     else
       let
         val (thms', thy') = thy
-          |> app_facts (map (apfst (name_thms name_flags1 name)) facts)
+          |> app_facts (name_facts name_flags1 name facts)
           |>> name_thms name_flags2 name |-> register;
         val thy'' = thy' |> add_facts (b, Lazy.value thms');
       in (map (Thm.transfer thy'') thms', thy'') end