src/HOL/List.thy

--- a/src/HOL/List.thy	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/List.thy	Sun Aug 04 13:24:54 2024 +0200
@@ -670,7 +670,7 @@
   | tac ctxt (Case (T, i) :: cont) =
       let
         val SOME {injects, distincts, case_thms, split, ...} =
-          Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
+          Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name T)
       in
         (* do case distinction *)
         Splitter.split_tac ctxt [split] 1