diff -r 33749040b6f8 -r 16e98f89a29c src/Pure/Isar/generic_target.ML
--- 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)