# HG changeset patch
# User wenzelm
# Date 1754564802 -7200
# Node ID d3774dbb305ecdf0ad3e5cae7257411b69770360
# Parent  5f03fb28849da625723492aeef9f250d4c4c307e
tuned proofs;

diff -r 5f03fb28849d -r d3774dbb305e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Aug 07 13:02:14 2025 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 07 13:06:42 2025 +0200
@@ -1733,10 +1733,10 @@
 lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))" (is "?lhs = ?rhs")
 proof (intro iffI allI)
   assume L: ?lhs
-  then have \<section>: "\<forall>x. P x (THE y. P x y)"
+  then have *: "\<forall>x. P x (THE y. P x y)"
     by (best intro: theI')
   show ?rhs
-    by (rule ex1I) (use L \<section> in \<open>fast+\<close>)
+    by (rule ex1I) (use L * in \<open>fast+\<close>)
 next
   fix x
   assume R: ?rhs