# HG changeset patch
# User nipkow
# Date 1591177461 -7200
# Node ID 4c5778d8a53df6e81dfe4198c0aba4101072c904
# Parent  435cdc77211019bbf5915aac7bf44c7916e0cc8e
should have been copied across from Set.thy as well for better printing

diff -r 435cdc772110 -r 4c5778d8a53d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat May 30 11:48:35 2020 +0000
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 03 11:44:21 2020 +0200
@@ -189,6 +189,11 @@
   "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
   "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
 
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>,
+  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
 lemma count_eq_zero_iff:
   "count M x = 0 \<longleftrightarrow> x \<notin># M"
   by (auto simp add: set_mset_def)