--- a/src/Pure/Isar/generic_target.ML Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Dec 24 11:51:59 2023 +0100
@@ -349,9 +349,6 @@
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 o apsnd o map o apfst o map) f;
in
@@ -360,7 +357,7 @@
let
val facts' = facts |> map (fn (a, thms) =>
let
- val name_pos = bind_name lthy (fst a);
+ 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';