| changeset 79371 | a2fbac74fba7 |
| parent 79368 | a2d8ecb13d3f |
| child 79372 | d02c8adce4e6 |
--- 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;