diff -r dff445a16252 -r 243f6bec771c src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sat Oct 19 17:16:16 2024 +0200 +++ b/src/HOL/Library/FSet.thy Sat Oct 19 19:00:19 2024 +0200 @@ -215,9 +215,9 @@ "\x|\|A. P" \ "CONST fBall A (\x. \ P)" "\!x|\|A. P" \ "\!x. x |\| A \ P" -print_translation \ - [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\fBall\ \<^syntax_const>\_fBall\, - Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\fBex\ \<^syntax_const>\_fBex\] +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\)] \ \ \to avoid eta-contraction of body\ syntax