diff -r 27d5452d20fc -r 4041e7c8059d src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -446,7 +446,7 @@
       let
         val (p, args) = strip_comb t
         val mode = Predicate_Compile_Core.head_mode_of derivation
-        val name = fst (dest_Const p)
+        val name = dest_Const_name p
 
         val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode)))
         val args' = map (translate_term ctxt constant_table') args