# HG changeset patch
# User wenzelm
# Date 1703415980 -3600
# Node ID 8aca79b3a9cb8333eebc4ef9117a486d021f211d
# Parent  f86c310327dfd723ce6aa150dcdfd74ad1a3e50e
clarified modules;

diff -r f86c310327df -r 8aca79b3a9cb src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Dec 24 11:58:33 2023 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Dec 24 12:06:20 2023 +0100
@@ -31,6 +31,9 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val map_thms: ('a -> 'b) ->
+    ('c * ('a list * 'd) list) list ->
+    ('c * ('b list * 'd) list) list
   val trim_context_binding: Attrib.binding -> Attrib.binding
   val trim_context_thms: thms -> thms
   val trim_context_fact: fact -> fact
@@ -186,6 +189,8 @@
 fun map_facts f = map (fn (a, b) => (apsnd f a, (map o apsnd) f b));
 fun map_facts_refs f g = map_facts f #> (map o apsnd o map o apfst) g;
 
+fun map_thms f = (map o apsnd o map o apfst o map) f;
+
 
 (* implicit context *)
 
diff -r f86c310327df -r 8aca79b3a9cb src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 11:58:33 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 12:06:20 2023 +0100
@@ -349,8 +349,6 @@
 
   in (result'', result) end;
 
-fun map_facts f = (map o apsnd o map o apfst o map) f;
-
 in
 
 fun notes target_notes kind facts lthy =
@@ -360,8 +358,8 @@
         val name_pos = Local_Theory.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';
+    val local_facts = Attrib.map_thms #1 facts';
+    val global_facts = Attrib.map_thms #2 facts';
   in
     lthy
     |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)