diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -270,8 +270,8 @@
       end
     fun flat_intro intro (new_defs, thy) =
       let
-        val constname = fst (dest_Const (fst (strip_comb
-          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro))))))
+        val constname = dest_Const_name (fst (strip_comb
+          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro)))))
         val (intro_ts, (new_defs, thy)) =
           fold_map_atoms (process constname) (Thm.prop_of intro) (new_defs, thy)
         val th = Skip_Proof.make_thm thy intro_ts