src/HOL/Library/Permutation.thy

--- a/src/HOL/Library/Permutation.thy	Thu Jun 16 17:11:00 2016 +0200
+++ b/src/HOL/Library/Permutation.thy	Fri Jun 17 12:37:43 2016 +0200
@@ -135,7 +135,7 @@
   done
 
 proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
-  apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
+  apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
   apply (insert surj_mset)
   apply (drule surjD)
   apply (blast intro: sym)+