diff -r 8a9588ffc133 -r a1162cbda70c src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Fri Jun 07 23:53:31 2024 +0200
+++ b/src/Pure/thm_name.ML	Sat Jun 08 11:23:40 2024 +0200
@@ -48,9 +48,9 @@
 
 val none: P = (empty, Position.none);
 
-fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)]
-  | list ("", pos) thms = map (fn thm => ((empty, pos), thm)) thms
-  | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
+fun list (name, pos) [x] = [(((name, 0), pos): P, x)]
+  | list ("", pos) xs = map (fn thm => ((empty, pos), thm)) xs
+  | list (name, pos) xs = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) xs;
 
 fun expr name = burrow_fst (burrow (list name));