# HG changeset patch
# User wenzelm
# Date 1703417702 -3600
# Node ID df48a5b8550631c6955a88d6f30db0e14fd9e79e
# Parent  670b3dc1daeedc02b4fef693d149da7ee50bbdd0
tuned;

diff -r 670b3dc1daee -r df48a5b85506 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 12:32:25 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 12:35:02 2023 +0100
@@ -349,16 +349,14 @@
 
   in (result'', result) end;
 
-fun burrow_fact f = split_list #>> burrow f #> op ~~;
+fun name_thms name = split_list #>> burrow (Global_Theory.name_multi name) #> op ~~;
 
 in
 
 fun notes target_notes kind facts lthy =
   let
     val facts' = facts |> map (fn (a, thms) =>
-      let
-        val name_pos = Local_Theory.bind_name lthy (fst a);
-        val thms' = burrow_fact (Global_Theory.name_multi name_pos) thms;
+      let val thms' = name_thms (Local_Theory.bind_name lthy (fst a)) thms;
       in (a, (map o apfst o map) (import_export_proof lthy) thms') end);
     val local_facts = Attrib.map_thms #1 facts';
     val global_facts = Attrib.map_thms #2 facts';