diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -951,7 +951,7 @@
 
 fun case_betapply thy t =
   let
-    val case_name = fst (dest_Const (fst (strip_comb t)))
+    val case_name = dest_Const_name (fst (strip_comb t))
     val Tcon = datatype_name_of_case_name thy case_name
     val th = instantiated_case_rewrite thy Tcon
   in
@@ -1068,7 +1068,7 @@
           let
             val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
               handle Type.TYPE_MATCH =>
-                error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
+                error ("Type mismatch of predicate " ^ dest_Const_name pred ^
                   " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
                   " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
                   " in " ^ Thm.string_of_thm ctxt' th)
@@ -1077,7 +1077,7 @@
           let
             val (pred', _) = strip_intro_concl th
             val _ =
-              if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+              if not (dest_Const_name pred = dest_Const_name pred') then
                 raise Fail "Trying to instantiate another predicate"
               else ()
             val instT =