diff -r dff445a16252 -r 243f6bec771c src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Oct 19 17:16:16 2024 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Oct 19 19:00:19 2024 +0200 @@ -180,9 +180,9 @@ "\x\#A. P" \ "CONST Multiset.Ball A (\x. P)" "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)" -print_translation \ - [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\Multiset.Ball\ \<^syntax_const>\_MBall\, - Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\Multiset.Bex\ \<^syntax_const>\_MBex\] +typed_print_translation \ + [(\<^const_syntax>\Multiset.Ball\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBall\), + (\<^const_syntax>\Multiset.Bex\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBex\)] \ \ \to avoid eta-contraction of body\ lemma count_eq_zero_iff: