diff -r ac6a69b0f634 -r f9b31d348fde src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Aug 18 15:41:55 2024 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sun Aug 18 15:49:24 2024 +0200
@@ -18,9 +18,8 @@
 fun mk_definitional [] arg = arg
   | mk_definitional ((thname, cname, covld) :: cos) (thy, thm) =
       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        Const (\<^const_name>\<open>Ex\<close>, _) $ P =>
+        \<^Const_>\<open>Ex ctype for P\<close> =>
           let
-            val ctype = domain_type (type_of P)
             val cname_full = Sign.intern_const thy cname
             val cdefname =
               if thname = ""