--- 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