# HG changeset patch
# User wenzelm
# Date 1703414780 -3600
# Node ID 704aea7f5203043e1c4d0a629cf41506bc371725
# Parent  5071516d45a637addd867f6ab98c8d65b85c3df2
tuned;

diff -r 5071516d45a6 -r 704aea7f5203 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 11:18:16 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 11:46:20 2023 +0100
@@ -352,16 +352,17 @@
 fun bind_name lthy b =
   (Local_Theory.full_name lthy b, Binding.default_pos_of b);
 
-fun map_facts f = map (apsnd (map (apfst (map f))));
+fun map_facts f = (map o apsnd o map o apfst o map) f;
 
 in
 
 fun notes target_notes kind facts lthy =
   let
-    val facts' = facts
-      |> map (fn (a, bs) =>
-          (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
-      |> map_facts (import_export_proof lthy);
+    val facts' = facts |> map (fn (a, thms) =>
+      let
+        val name_pos = bind_name lthy (fst a);
+        val thms' = Global_Theory.burrow_fact (Global_Theory.name_multi name_pos) thms;
+      in (a, (map o apfst o map) (import_export_proof lthy) thms') end);
     val local_facts = map_facts #1 facts';
     val global_facts = map_facts #2 facts';
   in