src/HOL/List.thy

--- a/src/HOL/List.thy	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/List.thy	Sun Aug 04 17:39:47 2024 +0200
@@ -639,7 +639,7 @@
             (case possible_index_of_singleton_case (fst (split_last args)) of
               SOME i =>
                 let
-                  val constr_names = map (fst o dest_Const) ctrs
+                  val constr_names = map dest_Const_name ctrs
                   val (Ts, _) = strip_type T
                   val T' = List.last Ts
                 in SOME (List.last args, T', i, nth args i, nth constr_names i) end