--- a/src/HOL/Tools/choice_specification.ML Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML Fri Dec 22 21:03:16 2023 +0100
@@ -28,9 +28,10 @@
else thname
val def_eq =
Logic.mk_equals (Const (cname_full, ctype), HOLogic.choice_const ctype $ P)
- val (thms, thy') =
- Global_Theory.add_defs covld [((Binding.name cdefname, def_eq), [])] thy
- val thm' = [thm,hd thms] MRS @{thm exE_some}
+ val (def_thm, thy') =
+ (if covld then Global_Theory.add_def_overloaded else Global_Theory.add_def)
+ (Binding.name cdefname, def_eq) thy
+ val thm' = [thm, def_thm] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
end