diff -r 6e28f282b37c -r a2fbac74fba7 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:34:47 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:50:17 2023 +0100
@@ -296,7 +296,7 @@
 
 local
 
-fun name_thms name = split_list #>> burrow (Thm_Name.make_list name) #> op ~~;
+fun name_thms name = split_list #>> burrow (Thm_Name.list name) #> op ~~;
 
 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;