diff -r 8c3eec5812d8 -r ae44f16dcea5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Feb 16 17:01:40 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Feb 16 22:28:19 2016 +0100
@@ -2302,12 +2302,18 @@
 lemma ex_mset: "\<exists>xs. mset xs = X"
   by (induct X) (simp, metis mset.simps(2))
 
+inductive pred_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> bool"
+where
+  "pred_mset P {#}"
+| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (M + {#a#})"
+
 bnf "'a multiset"
   map: image_mset
   sets: set_mset
   bd: natLeq
   wits: "{#}"
   rel: rel_mset
+  pred: pred_mset
 proof -
   show "image_mset id = id"
     by (rule image_mset.id)
@@ -2334,16 +2340,13 @@
       done
     done
   show "rel_mset R =
-    (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
-    BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)" for R
-    unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
+    (\<lambda>x y. \<exists>z. set_mset z \<subseteq> {(x, y). R x y} \<and>
+    image_mset fst z = x \<and> image_mset snd z = y)" for R
+    unfolding rel_mset_def[abs_def]
     apply (rule ext)+
-    apply auto
-     apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
-        apply (metis list_all2_lengthD map_fst_zip mset_map)
-       apply (auto simp: list_all2_iff)[1]
-      apply (metis list_all2_lengthD map_snd_zip mset_map)
-     apply (auto simp: list_all2_iff)[1]
+    apply safe
+     apply (rule_tac x = "mset (zip xs ys)" in exI;
+       auto simp: in_set_zip list_all2_iff mset_map[symmetric])
     apply (rename_tac XY)
     apply (cut_tac X = XY in ex_mset)
     apply (erule exE)
@@ -2355,6 +2358,16 @@
     done
   show "z \<in> set_mset {#} \<Longrightarrow> False" for z
     by auto
+  show "pred_mset P = (\<lambda>x. Ball (set_mset x) P)" for P
+  proof (intro ext iffI)
+    fix x
+    assume "pred_mset P x"
+    then show "Ball (set_mset x) P" by (induct pred: pred_mset; simp)
+  next
+    fix x
+    assume "Ball (set_mset x) P"
+    then show "pred_mset P x" by (induct x; auto intro: pred_mset.intros)
+  qed
 qed
 
 inductive rel_mset'