diff -r dfd5f665db69 -r 6f8a56a6b391 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Fri Dec 06 15:20:43 2024 +0100 +++ b/src/HOL/Library/FSet.thy Fri Dec 06 20:26:33 2024 +0100 @@ -216,8 +216,8 @@ "\!x|\|A. P" \ "\!x. x |\| A \ P" typed_print_translation \ - [(\<^const_syntax>\fBall\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBall\), - (\<^const_syntax>\fBex\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBex\)] + [(\<^const_syntax>\fBall\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBall\), + (\<^const_syntax>\fBex\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBex\)] \ \ \to avoid eta-contraction of body\ syntax