diff -r fe0b52983b7b -r a2d8ecb13d3f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 13:17:55 2023 +0100
@@ -366,7 +366,7 @@
     val (facts', lthy') =
       (facts, lthy) |-> fold_map (fn (a, thms) => fn lthy1 =>
         let
-          val thms1 = name_thms (Local_Theory.bind_name lthy1 (fst a)) thms;
+          val thms1 = name_thms (Local_Theory.full_name_pos lthy1 (fst a)) thms;
           val (thms2, lthy2) =
             (thms1, lthy1) |-> fold_map (fn (args, atts) =>
               fold_map thm_definition args #>> rpair atts);