diff -r 3f577308551e -r 293ede07b775 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Apr 26 22:44:31 2016 +0200
@@ -2075,7 +2075,7 @@
     "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
 proof -
   from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
-    "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+    "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
   moreover from this(3) [of a] have "a \<notin># K" by auto
   ultimately show thesis by (auto intro: that)
 qed