--- 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