--- a/src/Pure/Isar/generic_target.ML Fri Aug 16 10:04:47 2019 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Aug 16 10:20:41 2019 +0200
@@ -306,6 +306,8 @@
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))));
+
in
fun notes target_notes kind facts lthy =
@@ -313,9 +315,9 @@
val facts' = facts
|> map (fn (a, bs) =>
(a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
- |> Global_Theory.map_facts (import_export_proof lthy);
- val local_facts = Global_Theory.map_facts #1 facts';
- val global_facts = Global_Theory.map_facts #2 facts';
+ |> map_facts (import_export_proof lthy);
+ val local_facts = map_facts #1 facts';
+ val global_facts = map_facts #2 facts';
in
lthy
|> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)