tuned;

--- a/src/Pure/Isar/proof_context.ML	Sun Dec 24 11:13:33 2023 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Dec 24 11:13:54 2023 +0100
@@ -1054,10 +1054,10 @@
     val (name, pos) = bind_name ctxt b;
     val facts' = facts
       |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos));
-    fun app (ths, atts) =
+    fun app_fact (ths, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
-    val (res, ctxt') = fold_map app facts' ctxt;
-    val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res);
+    val (res, ctxt') = fold_maps app_fact facts' ctxt;
+    val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) res;
     val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
   in ((name, thms), ctxt'') end;
 

--- a/src/Pure/global_theory.ML	Sun Dec 24 11:13:33 2023 +0100
+++ b/src/Pure/global_theory.ML	Sun Dec 24 11:13:54 2023 +0100
@@ -307,7 +307,7 @@
 local
 
 val app_facts =
-  apfst flat oo fold_map (fn (thms, atts) => fn thy =>
+  fold_maps (fn (thms, atts) => fn thy =>
     fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
 
 in