--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -68,7 +68,7 @@
       let
         val name =
           singleton (Name.variant_list names)
-            ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+            ("specialised_" ^ Long_Name.base_name (dest_Const_name pred))
         val bname = Sign.full_bname thy name
       in
         if Sign.declared_const thy bname then