--- a/src/HOL/Library/Multiset.thy Fri Mar 18 10:14:56 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 18 12:48:00 2016 +0100
@@ -2062,7 +2062,7 @@
done
lemma one_step_implies_mult:
- "trans r \<Longrightarrow> J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
+ "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
\<Longrightarrow> (I + K, I + J) \<in> mult r"
using one_step_implies_mult_aux by blast