diff -r 06ab0a304f29 -r b275e3379024 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 20:40:15 2023 +0100
@@ -296,8 +296,8 @@
 
 local
 
-val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.flatten;
-val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.flatten;
+val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.short;
+val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.short;
 
 fun thm_def (name, pos) thm lthy =
   if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then