--- 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 *)
--- 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)