src/Pure/Isar/generic_target.ML

   in (result'', result) end;
 
 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 =
   let
     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)
     |> Attrib.local_notes kind local_facts
   end;