# HG changeset patch
# User wenzelm
# Date 1723400387 -7200
# Node ID 58a209c8d40abbb90ff687334e3b0c4feed67470
# Parent  e451d6230535732c828bd66f0c0355925b8403f1
tuned;

diff -r e451d6230535 -r 58a209c8d40a src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Aug 11 14:45:56 2024 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Aug 11 20:19:47 2024 +0200
@@ -101,7 +101,7 @@
 val typedef_overloaded = Attrib.setup_config_bool \<^binding>\<open>typedef_overloaded\<close> (K false);
 
 fun mk_inhabited T A =
-  HOLogic.mk_Trueprop (\<^Const>\<open>Ex T for \<open>Abs ("x", T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> A\<close>)\<close>\<close>);
+  \<^instantiate>\<open>'a = T and A in prop \<open>\<exists>x::'a. x \<in> A\<close>\<close>;
 
 fun mk_typedef newT oldT RepC AbsC A =
   let val type_definition = \<^Const>\<open>type_definition newT oldT for RepC AbsC A\<close>